Logika. Výroková logika Luboš Popelínský E-mail: popel@fi.muni.cz http://nlp.fi.muni.cz/uui/ Obsah: o Logika a umělá inteligence • Logický agent • Výroková logika • Splnitelnost o SAT problém Úvod do umělé inteligence 5/12 1/26 Logika a umělá inteligence místo úvodu You can think about deep learning as equivalent to ... our visual cortex or auditory cortex. But, of course, true intelligence is a lot more than just that, you have to recombine it into higher-level thinking and symbolic reasoning, a lot of the things classical Al tried to deal with in the 80s. ... We would like to build up to this symbolic level of reasoning - maths, language, and logic. So that's a big part of our work. Demis Hassabis, CEO and co-founder of Google Deepmind Úvod do umělé inteligence 5/12 2/26 Logika a umělá inteligence místo úvodu You can think about deep learning as equivalent to ... our visual cortex or auditory cortex. But, of course, true intelligence is a lot more than just that, you have to recombine it into higher-level thinking and symbolic reasoning, a lot of the things classical Al tried to deal with in the 80s. ... We would like to build up to this symbolic level of reasoning - maths, language, and logic. So that's a big part of our work. Demis Hassabis, CEO and co-founder of Google Deepmind Úvod do umělé inteligence 5/12 3/26 Príklad Logika a umělá inteligence Pokud X + Y=10aX-Y = 4, kolik je X? jak řešit • prohledávat prostor všech možných řešení např. do hloubky, kontrolovat platnost obou omezujících podmínek • CSP (Constraint Satisfaction problem) s proměnnými X a Y, • sečíst obě rovnice a vydělit 2. Použili jsme operace zachovávající pravdivost tj. odvozování založené na logice, logickou inferenci Úvod do umělé inteligence 5/12 4/26 O krok zpět Logika a umělá inteligence (zjednodušený) kognitivní proces: data -» UČENÍ -» model dotaz —>► INFERENCE pomocí modelu —> odpověď Úvod do umělé inteligence 5/12 5/26 O krok zpět Logika a umělá inteligence (zjednodušený) kognitivní proces: data -> UČENÍ -> model INDUKCE dotaz INFERENCE pomocí modelu odpověď DEDUKCE INDUKCE odvozuje generalizaci z dat, např. pravidla, DEDUKCE odvozuje logicky platný závěr na základě těchto pravidel Zde se soustředíme na na DEDUKCI, tj. na INFERENCI metodami logiky, Příklad: Eukleidův axiomatický systém pro geometrii Úvod do umělé inteligence 5/12 6/26 Logika Logika a umělá inteligence dva cíle 9 reprezentovat znalosti o doméně • umět odvozovat na základě těchto znalostí • logika = nástroj pro odvozování důsledků z předpokladů Úvod do umělé inteligence 5/12 7/26 • Znalostní báze (knowledge base, KB) = množina vět ve formálním jazyce 9 Deklarativní přístup k tvorbě agenta Tell it what it needs to know (or have it Learn the knowledge) ■ Then it can Ask itself what to do—answers should follow from the KB ■ pomocí inferenčního mechanismu • Znalostní systém může odpovědět v principu na libovolnou otázku (podle KB) 9 na rozdíl např. od prohledávacích algoritmů, kde typická otázka je "jak se dostat z A do B" Úvod do umělé inteligence 5/12 8/26 function KB-AGENT(percept) # vrací akci # globální: KB - báze znalostí; t - číslo, na začátku 0 tell {KB, make_percept_sentence(percepř, ť)) action ^— asW{KB, make_action_query(ř)) tell {KB, make_action_sentence(acř/OA7, ť)) t <- í+1 return action Úvod do umělé inteligence 5/12 9/26 Ex.: Pokud X + Y=10aX-Y = 4, kolik je X? KB-AGENT Pravidla do znalostní báze • if ((A=B) and (C=D)) then add((A+C)=(B+D)) • if (n*X=B) then add(X=B/n) Inferenční mechanismus - např. forward chaining (fix point semantics) Úvod do umělé inteligence 5/12 10 / 26 Otázky o jaký jazyk použít o co musí obsahovat KB • jaký má být inferenční mechanismus 9 existuje pro každou z těchto otázek minimální varianta? o k čemu je užitečný nejprve pro výrokovou logiku Úvod do umělé inteligence 5/12 11 / 26 Logický agent História Magistra Vitae ... ? https: //www.britannica.com/topic/history-of-logic a filozofická logika ■ Thalés z Milétu - geometrické věty a důkazy ■ Aristoteles - první formální systém, princip sporu, princip vyloučení třetího ■ Euklides - axiomy, větz, první axiomatický systém ■ stoikové 3.stol. př.n.l. - základy výrokové logiky • počátky symbolické logiky (13.- 19. století) ■ J. Duns Scotus - z dvou odporujících si tvrzení plyne cokoliv ■ W. Ockham - odlišil tvrzení a odvozovací pravidlo ■ G. W. Leibniz - idea logického kalkulu pro exaktní vědy ■ B. Bolzano - operace odvoditelnosti, kvantifikátory ■ G. Boole - Boolova algebra, fomální logika v moderním slova smyslu Úvod do umělé inteligence 5/12 12 / 26 20. století Logický agent matematická logika G. Frege, přelom století - axiomatizace výrokové logiky B. Russell, 1918 - objasnění paradoxu lháře C. S.Lewis, J.Lukasiewicz - neklasické logiky D. Hilbert, W. Ackermann - axiomatizace predikátového počtu úplnost výrokové (Post 1921) a predikátové (Goedel 1930) logiky K. Goedel - neúplnost systémů obsahujících aritmetiku, omezená možnost důkazu bezespornosti A.Church, 1936 - nerozhodnutelnost predikátové logiky A. Turing, 1937 - pojem vyčíslitelnosti, Turingův stroj ogika v informatice, v AI, výpočtová logika verifikace programů binary decision diagrams znalostní systémy logické programování Úvod do umělé inteligence 5/12 13 / 26 Logický agent História Magistra Vitae ... ! 9 filozofická logika ■ ■ Euklides - axiomy, věty, první axiomatický systém ■ • počátky symbolické logiky (13.- 19. století) ■ ■ G. Boole - Boolova algebra, formální logika v moderním slova smyslu, ale též he wrote a new book on The Laws of Thought with two parts: Logic + Probability ■ • matematická logika (konec 19. až polovina 20. stol.) ■ ■ A. Turing, 1937 - pojem vyčíslitelnosti, Turingův stroj, kolem 1950 -induktivní inference Úvod do umělé inteligence 5/12 14 / 26 Logical Agents. In Russell and Norvig. Al. A Modern Approach Anil Nerode, Richard A. Shore, Logic for Applications. Springer Verlag. základní kniha, mnohokrát v knihovně Fl Logic and Artificial Intelligence. In: Stanford Encyclopedia of Philosophy https://plato.stanford.edu/entries/logic-ai/ Úvod do umělé inteligence 5/12 15 / 26 Klasifikace logik Logický agent o formální (co je poznané, definované; metody odvozování) • neformální, mentální (co je poznatelné; zdravý selský rozum, komunikace mezi lidmi, heuristické odvozování) Formální logika • dvouhodnotová - true, falše, i vícehodnotová o extensionální - pravdivost formule závisí jen na pravdivosti jejich složek o intesionální - nejen na psti složek - "možná", "věřím" Dvouhodnotová extensionální logika zde • výroková Jestliže bude pěkně a nebudu učit, půjdu hrát tenis, p A -iq =4> r • predikátová ■ 1. řádu Není pravda, že všichni lidé jsou spokojení -iVx : ( člověk(x) spokojený(x)) ■ 2. řádu Existuje vlastnost, kterou mají všichni lidé 3PVx : ( člověk(x) P(x) ) Úvod do umělé inteligence 5/12 16 / 26 Výroková logika Výroková logika. Syntax • abeceda 1. výrokové symboly: p, q, r, s,..., případně pi, P2, P3 ... 2. symboly pro spojky: V, A, <^>, ... 3. pomocné symboly: (,) « správně utvořená formule (dále jen formule) 1. každý výrokový symbol je formule (tzv. atomická formule) 2. je-li výraz A formule, pak -*(A) je formule 3. jsou-li výrazy A, B formule, pak také (A) V (6), (A) A (6), (A) =>► (6), (/4) <^> (6), ... jsou formule 4. ... a případně pro další spojky ... 5. nic jiného není formule 9 není definována priorita binárních operátorů • závorková konvence: závorky lze vynechat, pokud to není na újmu jednoznačnosti formule Úvod do umělé inteligence 5/12 17 / 26 • nulární pravdivostní funkce (nezávislé na žádném argumentu) jsou konstanty odpovídající pravdivostním hodnotám 0, 1 o unární (jednoargumentové) spojky: F\ - unární verum, F2 - unární projekce p, F3 - negace p (ozn. -ip); F4 - unární falsum. • binární - A, V, =>►, <^>, ... • ternární - ternární A, ... , if X then Y else Z Úvod do umělé inteligence 5/12 18 / 26 Výroková logika Úplný systém logických spojek U každého jazyka nás zajímá nejen jeho expresivita (síla vyjádření). Existuje minimální dostatečná množina spojek? • prostřednictvím systému spojek {-i, A, V} dokážeme vyjádřit libovolnou spojku. • množinu spojek s touto vlastností nazýváme úplným systémem spojek • další úplné systémy např. {-i, A}, {-■, V}, {-", o jednoprvkové úplné systémy: Shefferova funkce NAND (negace konjunkce), Nicodova funkce NOR (negace disjunkce) Př. (p V q) & ((p | p) | (q | q)) Umíme systematicky hledat úplné systémy spojek? Jaké vlastnosti musí mít úplné systémy spojek? https: //en.wikipedia.org/wiki/Functional_completeness Úvod do umělé inteligence 5/12 19 / 26 Výroková logika Sémantika. Interpretace • Pravdivostní ohodnocení (interpretace) je funkce přiřazující všem atomickým formulím dané úvahy pravdivostní hodnoty (tj. každému výrokovému symbolu přiřadí 0 nebo 1). • Valuace je rozšíření interpretace z atomických na všechny formule dle tabulky pro výrokové spojky (přiřadí 0 nebo 1 např. i p A -iq). • Interpretace / splňuje formuli A (formule je pravdivá v /, resp. odpovídající valuace ľ(A) = 1), pokud 1. A je výrokový symbol a l(A) = 1 2. A je -.6 a / nesplňuje 6, resp. ľ (B) = 0 3. A je tvaru B A C a / splňuje B i C, resp. ľ (B) = ľ (C) = 1 4. A je B V C b I splňuje 6 nebo C, resp. /'(B) = 1 nebo /'(C) = 1 5. A je tvaru B^> Ca / nesplňuje 6 nebo splňuje C, resp. ľ {B) = 0 nebo /'(C) = 1 6. /4 je B <^> C a / splňuje B i C nebo / nesplňuje B i C, resp. ^(6) = ^(C) Úvod do umělé inteligence 5/12 20 / 26 Splnitelnost Splnitelnost. Model formule • Mějme formuli ^pV p; všechny možné interpretace (existují dvě: /(p) = 1, /i(p) = 0) splňují tuto formuli. Formule, která je splňována každou interpretací, se nazývá tautologie. 9 Formule -ip A p není splňována žádnou z možných interpretací; takové formule nazýváme kontradikce. • Formule A je splnitelná, je-li splňována alespoň jednou interpretací. Tuto interpretaci označujeme jako model formule A. o Množina formulí T je splnitelná, pokud existuje interpretace splňující každou formuli z T. Tuto interpretaci nazýváme modelem množiny T. o Formule A logicky vyplývá (na základě výrok, logiky) z množiny T, pokud pro každý model / množiny T / splňuje A. Zapisujeme T |= A. Úvod do umělé inteligence 5/12 21 / 26 Splnitelnost Logický agent pro výpočet logického důsledku function TT-ENTAILS?(/C8,a) #returns true or false inputs :KB, the knowledge base, a sentence in propositional logic a, the query, a sentence in propositional logic symbol <— a list of the proposition symbols in KB and a return TT-CHECK-ALL(KB,asymbols,{}) function TT-CHECK-ALL(K'8,ce,symbols,model) returns true or false if EMPTY?(symbols) then if PL-TRUE?(KB,model)then return PL-TRUE?(,model) else return true //when KB is false, always return true else P <- FIRST(symbols) rest ^— REST(symbols) return (TT-CHECK-ALL(AC8,a,rest,model U P=true}) and TT-CHECK-ALL(K'8,a,rest,model U {P=false})) Úvod do umělé inteligence 5/12 22 / 26 Výroková formule je splnitelná, právě když existuje interpretace (tj substituce výrokových symbolů), která je modelem, tj. je pravdivá v této interpretaci. SAT problém: pro danou formuli najít takovou interpretaci nebo vrátit, že neexistuje. SAT problém je NP-uplný existují podproblémy, které jsou P-SAT a jsou užitečné? 2-SAT. Horn-SAT, monotónní formule 3-SAT? NP-úplný. Důkaz např. http://ktiml.mff.cuni.cz/ kucerap/NTIN090/NTIN090-poznamky.pdf Úvod do umělé inteligence 5/12 23 / 26 01234 5 673 012345678 Clause/symbol ratio m!n Clause/symbol ratio m/n (a) (b) Figure 7.19 (a) Graph showing the probability that a random 3-CNF sentence with n = 50 symbols is satisfiable, as a function of the clause/symbol ratio m/n. (b) Graph of the median run time (measured in number of iterations) for both DPLL and WALKSAT on random 3-CNF sentences. The most difficult problems have a clause/symbol ratio of about 4.3. Uvod do umele inteligence 5/12 24 / 26 Shrnutí SAT problém Víme, • co je interpretace (angl. assignement) • kdy je formule pravdivá v interpretaci (dtto interpretace splňuje formuli) • co je model formule a množiny formulí • co jsou tautologie a kontradikce • kdy formule logicky vyplývá z množiny formulí/je logickým důsledkem této množiny o co je úplný systém logických spojek (angl. functionally complete) Úvod do umělé inteligence 5/12 25 / 26 co je WalkSAT a DPLL? Pravdivost, dokazatelnost. Důkazové metody a systémy. Formální (deduktivní) systémy. Axiomatické systémy Úvod do umělé inteligence 5/12 26 / 26