r Predikátová logika II. Uvod do logického programování. Intensionální logiky Luboš Popelínský E-mail: popel@fi.muni.cz http://nip.fi.muni.cz/uui/ Obsah: o Normálni formy v predikátové logice • Skolemizace a unifikace • Rezoluce v predikátové logice • Logické programování Intensionální logiky_ Úvod do umělé inteligence 8/12 Obsah O Normální formy v predikátové logice Q Skolemizace a unifikace Q Rezoluce v predikátové logice Q Logické programování Q Intensionální logiky Úvod do umělé inteligence 8/12 2/45 Axiomatický systém predikátové logiky I • používáme spojky {=^,^} a kvantifikátor V. Ostatní spojky jsou chápány jako zkratky uvedené ve výr. logice, resp. 3xA -Nx^A 9 axiomy pro spojky (/4, 6, C jsou formule) - shodné s výr. logikou: A2 (A (B C)) {{A B)^(A^ C)) A3 (-.6 ^A) ^{A^ B) • axiomy pro V: A4 MxA A(x/t) A5 Vx(^ B) ^ (A^ŕ VxB), /4 neobsahuje volně x Úvod do umělé inteligence 8/12 3/45 Axiomatický systém predikátové logiky II • axiomy pro rovnost: A§ x = x A7 (x = y) (f(xi,... ,x/_i,x,x/+i,... ,x„) = f(xi,... ,x/_i,y,x/+i,... ,x„)) A8 (x = y) (P(xi,... ,X/_i,X,X/+i, ... ,x„) = P(xi,... ,x/_i,y,x/+i,... ,x„)) • odvozovací pravidla: ■ modus ponens (MP, stejné s výr. logikou): z A a A B odvodíme B pro libovolné formule A, B ■ generalizace (PG): z A odvodíme MxA Úvod do umělé inteligence 8/12 4/45 Axiomatický systém: příkla Příklad: důkaz z předpokladu. Ukažte, že pokud je dokazatelná formule A B a proměnná x není volná v A, pak je dokazatelná i formule A VxR 1. h A 6 předpoklad 2. hVx(/\^6) PG(1) 3. h Vx(/\ =>■ B) (4 VxB) A5 4. h/^VxB MP(2,3) Úvod do umělé inteligence 8/12 5/45 Využití axiomatického systému: teorie • teorie: množina uzavřených formulí T, model teorie T: interpretace, v níž je každá formule z T pravdivá Příklad: teorie elementární aritmetiky (0, unární funkce následník s, binární +,*) • Axi Vx^(s(x) = 0) Ax2 Vx(x + 0 = x) Ax3 VxVy(x + s(y) = s(x + y)) Ax4 Vx(x * 0 = 0) AX5 VxVy(x * s(y) = (x * y) + x) • pomocná odvozovací pravidla: (PS) je-li h x = y, pak h y = x (symetrie =) (PT) je-li hx = yahy = z, pak h x = z (tranzitivita =) (PPS) je-li h x = y, pak h s(x) = s(y) (přidání s) (PVS) je-li h s(x) = s(y), pak h x = y (vypuštění s) Úvod do umělé inteligence 8/12 6/45 Teorie: příklad důkazu Příklad: dokažte v teorii elementární aritmetiky s(0) + s(0) = s(s(0)). 1. h VxVy(x + s(y) = s(x + y)) Ax3 2. h (VxVy(x + s(y) = s(x + y))) (Vy(s(0) + s(y) = s(s(0)+y))) A4 3. h Vy(s(0) + s(y) = s(s(0) + y)) MP(1,2) 4. h (Vy(s(0) + s(y) = s(s(0) + y))) (s(0) + s(0) = s(s(0) + 0)) A4 5. h s(0) + s(0) = s(s(0) + 0) MP(3,4) 6. h Vx(x + 0 = x) Ax2 7. h (Vx(x + 0 = x)) => (s(0) + 0 = s(0)) A4 8. hs(0) + 0 = s(0) MP(6,7) 9. h s(s(0)+ 0) = s(s(0)) PPS(8) 10. h s(0) + s(0) = s(s(0)) PT(5,9) Úvod do umělé inteligence 8/12 7/45 Normální formy v predikátové logice Normální formy v predikátové logice Prenexová normální forma (pnf) • cíl: převést libovolnou (uzavřenou) formuli do tvaru, v němž jsou všechny kvantifikátory na začátku a následuje otevřené (= bez kvantifikátorů) jádro v nkf (ndf) Qxi... Qxn^A^ V ... V ) A (A2l V ... V A2,2) A ... A {Ami V ... V Amim)) • příklad: VxVy3zVw((P(x,y) V -Q(z)) A (/?(x, w) V /?(y, w))) 9 Věta: pro každou formuli existuje ekvivalentní formule v konjunktivní (disjunktivní) prenexové normální formě. Úvod do umělé inteligence 8/12 8/45 Normální formy v predikátové logice Prenexová normální forma: algoritmus převodu 1. eliminovat zbytečné kvantifikátory 2. přejmenovat korektně proměnné tak, aby u každého kvantifikátoru byla jiná proměnná 3. eliminovat všechny spojky různé od -i, A a V 4. přesunout negaci dovnitř, je-li potřeba: -\/xA nahradit 3x^/4 -■(v4 A B) nahradit V -.6 apod. 5. přesunout kvantifikátory doleva (o e {A, V}, Q e {V, 3}): A o QxB nahradit Qx(A o B) QxA o B nahradit Qx(A o B) 6. použít distributivní zákony k převodu jádra do nkf (ndf): A V (B A C) nahradit (A V B) A (A V C) (A A 6) V C nahradit (>4 V C) A(BVC) Úvod do umělé inteligence 8/12 9/45 Normální formy v predikátové logice Převod do pnf - příklad Příklad: převeďte do konjunktivní pnf formuli Vx3y^(P(x,y) => Vz/?(y)) V -3xC?(x). 1. Vx3y^(P(x,y) R(y)) V ^3xQ(x) (zbytečné Vz) 2. Vxi3y-i(P(xi,y) P(y)) V -i3x2(?(x2) (přejmenování x) 3. Vxi3y-.(-.P(xi,y) V P(y)) V ^3x2(?(x2) (eliminace 4. Vxi3y(P(xi,y) A ->/?(y)) Wx2^(?(x2) (přesun negace 2x) 5. Vxi(3y(P(xi,y) A ->R(y)) Wx2^Q(x2)) (posun Vxi doleva) Vxi3y((P(xi,y) A ->P(y)) Wx2^Q(x2)) (posun 3y doleva) Vxi3yVx2((P(xi,y) A ->R(y)) V -iQ(x2)) (posun Vx2 doleva) 6. Vxi3yVx2((P(xi,y) V -./?(y) V -> = {x/h{f{b)),z/g{y,f{b)),w/y} S = {f(h(y),g(W)),^P(W,h(y)),Q(W,g(w,y),a)} S{U) = (S0)V = {f(h{f(b)),g(y)), -P(y, = = • • • = En(f), tedy v případě, že Sej) má jediný prvek. Existuje-li unifikátor množiny, označíme ji jako unifikovatelnou. • příklady: 1. {P(x, a), P(fa, c)}, {P(f(x), z), P(a, {P(x, -.P(a, {P(x,y, z), P(a, fa)}, {/?(x), P(x)} nejsou unifikovatelné 2. unifikátorem {P(x, c), P(fa, c)} je 0 = {x/fa}; žádný jiný neexistuje 3. unifikátorem {P(/r(x),y), P(/r(a), 1/1/)} může být 0 = {x/a, y/1/1/}, ale také -0 = {x/a,y/a, w/a}, a = {x/a,y/fa, w/fa} atd. • unifikátor 0 množiny S je nejobecnějším unifikátorem (mgu) S, pokud pro libovolný unifikátor íp množiny S existuje substituce A taková, že (p\ = íp • příklad: v bodu 3. předchozího příkladu je mgu 2 = {w/b}, S2 = Si02 = {P(f(h(b),g(z)),h(b)),P(f(h(b)7g(a))7x),P(f(h(b),g(z)),h(b))} 3. D(S2) = {z, a}, 03 = {z/a}, S3 = S23 = {P(f(/t(6)>fir(a)), P(f(h(b),g(a)),x), P(f(h(b),g(a)), h(b))} 4. D(S3) = {/?(£>), x}, 04 = {x//7(6)},S4 = S304 = {P(f(Kí>),fir(a)), Kb)), P(f(h(b),g(a)), h(b)), P(f(h(b),g(a)), h(b))} 5. mgu(S) = {y/h(w)}{w/b}{z/a}{x/h(b)} = {y/h(b),w/b,z/a,x/h(b)} Úvod do umělé inteligence 8/12 23 / 45 Rezoluce. Úvod Rezoluce v predikátové logice • metoda založená na vyvracení, pracujeme s formulemi ve Skolemově normální formě, kvantifikátory nepíšeme • jako ve výrokové logice: formuli VxVy((P(x, f(x)) V -"(?(/)) A (-./?(f(x)) V ->(?(y))) reprezentujeme jako {{P(x, r(x)), -Q(y)}, (x)), - 0(y)}} Standardizace proměnných • proměnné chápeme jako lokální v dané klauzuli (pozn.: Vx(4(x) A 6(x)) ^ (Vxrt(x) A VxS(x)) ^ (Vxrt(x) A VyS(y))) • mezi stejnými proměnnými v různých klauzulích není žádná vazba • standardizace proměnných: přejmenujeme proměnné v různých klauzulích tak, aby v nich žádné stejně pojmenované proměnné nevystupovaly • standardizace proměnných je nezbytná, příklad: {{P(x)}, {^P(/r(x))}} je nesplnitelná ^ bez přejmenování P(x) a P(/r(x)) nezunifikujeme 44> a bez unifikace nemůžeme rezolvovat Úvod do umělé inteligence 8/12 24 / 45 Rezoluce v predikátové logice Rezoluční pravidlo pro predikátovou logiku • rezoluční pravidlo pro predikátovou logiku: mějme klauzule C\ a C2 bez společných proměnných (po případném přejmenování) ve tvaru Ci = C[ U {P(xi),..., P(x„)}, C2 = C2 U {-P(ýi),..., -P(ý™)}. Je-li 0 mgu množiny {P(j?i),..., P(xn), ^(yi)? • • • 5 P(ym)}- pak rezolventou Ci a C2 je C[(f) U C20. • rezoluční důkazy a rezoluční vyvrácení definujeme stejně jako ve výrokové logice, pouze používáme rezoluční pravidlo pro predikátovou logiku: ■ rezoluční důkaz C z S je binární strom s listy z S a kořenem C, jehož každý vnitřní uzel je rezolventou svých bezprostředních následníků, ■ rezoluční vyvrácení S je rezoluční důkaz □ z S Úvod do umělé inteligence 8/12 25 / 45 Rezoluce v r. )redikátové logice Rezolventa - příklad ly 1 1 Př. 1: rezolvujeme klauzule {P(x, a)} a {^P(x,x)} • přejmenujeme proměnné např. v první klauzuli: {P(xi,a)} • mgu({P(xua),P(x,x)}) = {xi/a,x/a} • rezolventa □ Př. 2: rezolvujeme klauzule {P(x,y), -i/?(x)} a {^P(a, b)} • m^({P(x,y),P(a,b)}) = {x/a,y/b} o aplikujeme mgu na {^P(x)} • rezolventa {^P(a)} Úvod do umělé inteligence 8/12 26 / 45 Rezoluce v r. )redikátové logice Rezolventa - příklad ly 1 1 Př. 3: rezolvujeme klauzule Q = {Q(x),^R(y), P(x,y), P(f(z), f (z))} a C2 = {^N(u), ^R(w), -P(ŕ(a), f (a)), -P(r», f(w))} 9 vybereme množinu literálů, na kterých budeme rezolvovat {P(x,y), P(f(z), f (z)), P(f(a), f (a)), P(f(w), f(w))} • její mgu 0 = {x/f(a),y/f{a),z/a, w/a] • C[ = {(?(x),--/?(/)}, CÍ0 = {(?(f(a)),-./?(f(a))} • c£ = {-./V(!/),-./?(w)}, C^ = {-./V(i/),-./?(a)} • výsledná rezolventa C[0U = {C?(r(a)),-./?(f(a)),-./V(u),-./?(a)} Úvod do umělé inteligence 8/12 27 / 45 o obecné schméma důkazu ,A je důsledkem množiny formulí T': všechny prvky T a -iA převedeme do klauzulární formy, dokazujeme nesplnitelnost jejich sjednocení • poznámka: při jednom rezolučním kroku musíme být schopni odstranit několik literálů zároveň (pokud bychom v následujícím příkladu rezolvovali vždy pouze na jediném literálu, množinu rezolučně nevyvrátíme) • příklad: ukažte rezoluční vyvrácení {{P(x), P(y)}, {-"P(xi), ^P(yi)}} {P(x),P(y)} {-P(xi),-P(yi)} □ Úvod do umělé inteligence 8/12 28 / 45 Rezoluce v predikátové logice Rezoluční důkaz - příklad I Z předpokladu reflexivity VxP(x,x) a vlastnosti \/xÍy\Jz{{P{x,y) A P(y,z)) =4> P(z,x)) dokažte symetrii VxVy(P(x,y)^P(y,x)). • převedeme předpoklady do klauzulárního tvaru: 51 = {{P(x,x)}} 52 = {{^P(x,y)^P(y,z),P(z,x)}} 9 dokazovanou formuli negujeme: 3x3y(P(x,y)A-P(y,x)), převedeme do klauzulárního tvaru (přes Skolemovu nf): P(a, b)A^P(b, a) S = {{P(a,b)},{^P(b,a)}} • dokazujeme nesplnitelnost Si U S2 U S Úvod do umělé inteligence 8/12 29 / 45 Rezoluce v predikátové logice Rezoluční důkaz - příklad II « dokazujeme nesplnitelnost množiny klauzulí {{P(x, x)}, {-P(x, y), -P(y, z), P(z, x)}, {P(a, 6)}, {-P(b, a)}} o strom rezolučního vyvrácení (jeden z možných): y), -.P(y, z), a:)} {P(a, 6)} Úvod do umělé inteligence 8/12 30 / 45 Rezoluce v predikátové logice Rezoluce - vlastnosti • stejně jako ve výrokové logice je rezoluce v predikátové logice korektní a úplná • stejný problém jako ve výrokové logice: strategie generování rezolvent (příliš velký prohledávaný prostor) • lze použít všechny metody zjemnění uvedené pro výrokovou logiku (T-rezoluce, sémantická rezoluce atd.) • uvedeme pouze příklady variant rezoluce postupně směřujících k SLD-rezoluci (používané též v Prologu) Úvod do umělé inteligence 8/12 31 / 45 Rezoluce v predikátové logice Lineární rezoluce 9 lineární struktura důkazu, rezolvujeme vždy předchozí rezolventu s klauzulí z vyvracené množiny nebo dříve odvozenou rezolventou; korektní a úplná V/l III*// I v / s s v ■ 9 príklad: lineárni rezoluční vyvraceni množiny {{P(x, x)}, {-P(x,y), -nP(y, z), P(z, x)}, {P(a, />)}, {^P(b, a)}} {-.P(x, »), -.P(v, z),P(z, x)} {P(a, b)} x/a,y/b x/a,y/b {^P(b,z),P(z,a)} {-.P(M)} «/6 {-P(M)} {P(x,x)} s/6 a/6 Úvod do umělé inteligence 8/12 32 / 45 Rezoluce v predikátové logice Hornovy klauzule • omezení na určitý typ klauzulí používaných v programovacím jazyce Prolog • Hornova klauzule je klauzule s nejvýše jedním pozitivním literálem. Příklad: C = {p, -iq, ^r} Běžný zápis ve výrokové logice p V -iq V -ir lze ekvivalentními úpravami převést na p V Ar) a dále na p<^qAr, což v Prologu zapisujeme P :- q, r. a typy Hornových klauzulí: - programové s právě jedním pozitivním literálem dále dělíme na * fakta bez negativních lit. (př.: {p}, v Prologu p.) * pravidla s alespoň jedním negativním lit. (př.: {p, -iq}, p :- q.) - cíle bez pozitivního literálu (př.: {^p}, :- p. resp. ?- p.) • Každá nesplnitelná množina neprázdných Hornových klauzulí musí obsahovat alespoň jeden fakt a alespoň jeden cíl. Úvod do umělé inteligence 8/12 33 / 45 Rezoluce v predikátové logice Ll-rezoluce a LD-rezoluce • Ll-rezoluce - lineární rezoluce začínající cílovou klauzulí (žádný pozitivní literál), rezolvujeme vždy předchozí rezolventu (výhradně) s klauzulí z vyvracené množiny. Korektní, obecně není úplná; úplná pro Hornovy klauzule. o LD-rezoluce vychází z Ll-rezoluce, směřujeme k implementaci a pracujeme výhradně s Hornovými klauzulemi (nejvýše jeden pozitivní literál) • klauzule nahradíme uspořádanými klauzulemi; změna notace z {P(x),^R(x,f(y)),^Q(a)} na [P{x),^R{x,f(y)),^Q{a)] • rezoluce pro uspořádané klauzule v predikátové logice: mějme uspořádané klauzule bez společných proměnných (po případném přejmenování) G = [^AU^A2,... ,^An] a H = [Bo, """Bi? ^B2,..., ^Bm], rezolventou G a H pro (/) = mgu(Bo, Af) bude uspořádaná klauzule Úvod do umělé inteligence 8/12 34 / 45 Rezoluce v predikátové logice Neúplnost Ll-rezoluce {^} {q} {P} {p, ^q} {^p, q} {p, ^q} {^p, q} Úvod do umělé inteligence 8/12 35 / 45 Rezoluce v predikátové logice LD-rezoluce: příklad • LD-rezoluční vyvrácení množiny uspořádaných klauzulí {[P(x, x)], [P(z, x), -nP(x,y), -nP(y, z)], [P(a, />)], hP(f>, a)]} hP(6,o)] [P{z,x),-.P{x,v),^P(y,z)] x/a,z/b l-,P(a,y)^P(y,b)] {P(a,b)} [-iP(a, a □ Úvod do umělé inteligence 8/12 36 / 45 Rezoluce v predikátové logice S L D-rezoluce • pomocí selekčního pravidla algoritmizuje výběr literálu z cílové klauzule, na kterém se bude rezolvovat o SLD-rezoluce (s libovolným selekčním pravidlem) je korektní a úplná pro Hornovy klauzule budeme používat selekční pravidlo, které vybírá nejlevější literál • generování rezolvent pro uvedené pravidlo: G = [^A1^A2,...^An]1 H = [Bo, """Bi? ..., ~^Bm], rezolventou G a H pro (/) = mgu(Bo, Ai) je [->6i0, ^B2(t),..., ^Bmcf), -"y420,..., ^An(f)] Úvod do umělé inteligence 8/12 37 / 45 Rezoluce v predikátové logice SLD-rezoluce: příklad • příklad: SLD-rezoluční vyvrácení se zvoleným selekčním pravidlem (vybírajícím vždy nejlevější literál) hP(M)] [P(z,x)^P(x,y)^P(y7z)} x /a,z/b hP(a, y),-.?&,,&)] [P(a,ó)] hP(b,b)] [P(x,x)\ x/b □ • srovnání s LD-rezolucí: ve druhém kroku musíme rezolvovat na -iP(a, y) (v LD-rezoluci bylo možné vybrat libovolný z literálů -iP(a,y), ^P(y, b)) Úvod do umělé inteligence 8/12 38 / 45 Rezoluce v predikátové logice SLD-rezoluce: význam • máme množinu programových klauzulí P a cílovou klauzuli G = [^A1{x),...,^An{x)] • dokazujeme nesplnitelnost P U {G}, tj. P A Vx(-i^i(x) V ... V -*An(x)) 9 uvedená nesplnitelnost je ekvivalentní P I—iG, tj. Ph3x(^i(x)A... AAn(x)) 9 zadáním cíle G tedy chceme zjistit, zda existují nějaké objekty (případně jaké), které na základě P splňují formuli Ai(x) A ... A An{x) • aplikujeme-li kompozici všech mgu postupně použitých při SLD-odvození na jednotlivé proměnné vektoru x, získáme konkrétní příklady zmíněných objektů (termů) splňujících danou formuli Úvod do umělé inteligence 8/12 39 / 45 SLD -stromy Rezoluce v predikátové logice Prostor všech možných SLD-derivací při vyhodnocování daného cíle G pro program P dokážeme zachytit SLD-stromem. Příklad: 1 >P(x,x)] [-^Q(x,z),R(z,x)] >S(x)\ 8 [-^R{b,x)\ [-^R(a,b)][-^R(a,x),R(a,x)} [-^T(x,a)} [-^T(x,b)} [->T(x,x)] 6 11 10 ^[x/a] neúspěch neúspěch □ [x/b] ^[x/a] neúspěch Úvod do umělé inteligence 8/12 40 / 45 Logické programovaní Logické programovaní • strategie prohledávání stavového prostoru (SLD-stromu) do hloubky • výběr programových klauzulí shora dolů 9 výběr podcílů zleva doprava (viz selekční pravidlo v SLD rezoluci) • silně využívá rekurzi • historie: 70. I. 20. stol. - Colmerauer, Kowalski; D.H.D. Warren (WAM) • jazyk Prolog Úvod do umělé inteligence 8/12 41 / 45 Logické programovaní SLD-odvození pro logický program Přirozená čísla s nulou 0 G N A VX : ((X + 1) G N 4= X G N) + 1 s() naturalO(O). naturalO(s(X)) :- natural(X). —i num(s{s(0)) niim(s(X)), —■ num(X) —i num(s{0)) num(s{X)),—i num(X) \ X/0 —i num(O) num{0) —i num{0) num(O) Úvod do umělé inteligence 8/12 42 / 45 Logické programovaní říklad: Sčítaní dvou čísel x + Y = z VX : X + 0 = X VXVYVZ :X + (Y + 1) = (Z + 1)^X+Y = Z Peanova aritmetika: 1 = s(0), 2 = s(s(0))ľ s(Y) odpovídá Y + 1 plusl(X,0,X). plusl(X,s(Y),s(Z)) :- plusl(X,Y,Z). Úvod do umělé inteligence 8/12 43 / 45 Intensionálnř logiky Intensionální logiky Úvodem. Módy pravdy Cavaco Silva je presidentem Portugalska. Jana čte. Sluneční soustava má devět planet. (Nebo osm?) Třetí odmocnina z 27 jsou 3. nutně pravda, i v budoucnu. Ale: Jana ví, že třetí odmocnina z 27 jsou 3. Jan nevěří, že třetí odmocnina z 27 jsou 3. Verifikace programů: nejen různé světy, ale i různé budoucnosti VŽDY pravda, NĚKDY pravda, VÍM že, VĚŘÍM že, ... Úvod do umělé inteligence 8/12 44 / 45 Intensionálnř logiky Modálni logika □ 0 - "nutně platí 0", "0 je vždy pravda" Ocf) - "možná platí 0", "0 je někdy pravda Je-li C jazyk predikátové logiky, rozšíříme ho na modálni jazyk £n>o přidáním dvou symbolů □ and O do abecedy a do definice syntaxe přidáme Je-li (j) formule, pak také (n0) a (O0) jsou formule. Sémantika: Kripkeho rámce Úvod do umělé inteligence 8/12 45 / 45