Skolemizace. Důkazové systémy. Uvod do logického programování Luboš Popelínský E-mail: popel@fi.muni.cz http://nlp.fi.muni.cz/uui/ Obsah: • Skolemizace • Axiomatické systémy • Deduktivní systémy • Rezoluční metoda • Rezoluce v predikátové logice Úvod do umělé inteligence 7/12 1/51 Skolemovy normální formy. Skolemizace 9 převod formulí na formule bez existenčních kvantifikátorů v jazyce, který je rozšířen o tzv. Skolemovy funkce; zachovává splnitelnost • idea převodu: formuli Vxi... Vx„3yP(xi,... ,x„,y) transformujeme na Vxi... Vx„P(xi,..., x„, f(xi,..., x„)) a příklad: mějme celá čísla s +. Formuli Vx3y(x + y = 0) převedeme na Vx(x + f(x) — 0). Interpretace f - unární funkce, která pro daný argument vrátí opačné číslo. • Skolemova normální forma je prenexová normální forma pouze s univerzálními kvantifikátory. • Věta: každou formuli A lze převést na takovou formuli A' ve Skolemově normální formě, že A je splnitelná právě když A' je splnitelná. Úvod do umělé inteligence 7/12 2/51 Skolemizace Algoritmus převodu do Skolemovy nf 1. převést formuli do prenexové konjunktivní nf 2. provést Skolemizaci: odstranit všechny existenční kvantifikátory a nahradit jimi vázané proměnné pomocnými Skolemovými funkcemi • příklad 1: převeďte do Skolemovy nf formuli Vx3y-(P(x,y) Vz/?(y)) V -.3xQ(x) 1. Vxi3yVx2((P(xi,y) V -Q(x2)) A (-./?(y) V -Q(x2))) 2. VxiVx2((P(xi, f(xi)) V n(J(x2)) A (xi)) V -Q(x2))) příklad 2: převeďte do Skolemovy nf následující formuli v pnf Vx3yVz3u/(P(x,y) V ->Q(z, w)) 2. VxVz(P(x, fx(x)) V -C?(z, f2(x,z))) Úvod do umělé inteligence 7/12 3/51 Skolemizace Herbrandova věta I o motivace: hledáme snazší prostředky k určení, zda daná množina formulí je splnitelná • pracujeme s množinou S formulí ve Skolemově nf (univerzální kvantifikátory se často při zápisu vynechávají), jejími konstantami (alespoň jedna, příp. přidaná mimo S), funkčními a predikátovými symboly • Herbrandovo univerzum U(S) je množina všech uzavřených termů, které lze utvořit z konstant a funkčních symbolů z S (tzv. základní termy) př.: pro S = {P(f(0))} je U(S) = {0, f(0), f(f(0)), f(f(f(0))),...} 9 Herbrandova báze 6(S) je množina všech atomických formulí, které lze vytvořit nad prvky (V(S); 6(S) = {P(ti,..., tn)\ti £ U (S), P je predik. symbol figurující v S} př.: pro S = {P(f(0))} je B{S) = {P(0), P(f(0)), P(f(f(0))),... } Úvod do umělé inteligence 7/12 4/51 Skolemizace Herbrandova věta • Herbrandova interpretace je libovolná podmnožina báze 6(S) zahrnující ty aplikace predikátů na prvky univerza, které jsou pravdivé Poznámka: s funkcemi a konstantami lze pracovat i nadále pouze na symbolické úrovni • Herbrandův model M(S) množiny S je taková Herbrandova interpretace, ve které jsou všechny formule z S pravdivé • Herbrandova věta: buď existuje Herbrandův model S nebo existuje konečně mnoho uzavřených instancí prvků S, jejichž konjunkce neplatí • slabší tvrzení: S je splnitelná právě tehdy, když existuje její Herbrandův model • závěr: k rozhodnutí o splnitelnosti množiny již nepotřebujeme brát v úvahu všechny možné interpretace, stačí pracovat pouze se symbolickými' Herbrandovými interpretacemi Úvod do umělé inteligence 7/12 5/51 Skolemizace Herbrandovy modely - příklady Příklad 1: S = {P(0), P(s(x)) V -P(x)} (předp. V kvantifikovány) • U(S) = {0, s(0), s(s(0)), s(s(s(0))),... } B(S) = {P(0), P(s(0)), P(s(s(0))), P(s(s(s(0)))),... } M(S) = B(S) (minimální Herbrandův model je celá báze) poznámka: P vyjadřuje vlastnost ,být korektní přirozené číslo' (pomocí následníků nuly) Příklad 2: S' = {P(0), P(s(x)) V -P(x), R(x,s(x)) V -P(x)} • U(S') = {0, s(0), s(s(0)), s(s(s(0))),... } (stejné jako pro S) B(S') = {P(0), P(s(0)), P(s(s(0))), P(s(s(s(0)))),.. •, P(0,0), P(0, s(0)), P(s(0), 0), P(s(0), s(0)),... } M(S') = {P(0), P(s(0)), P(s(s(0))), P(s(s(s(0)))),. • •, R{0, s(0)), P(s(0), s(s(0))), P(s(s(0)), s(s(s(0))))... } poznámka: P je stejné jako pro S, /?(x,y) reprezentuje binární vlastnost ,y je následníkem x' (resp. ,x je předchůdcem y') Úvod do umělé inteligence 7/12 6/51 Axiomatické systémy Axiomatický systém pro výrokovou logiku • jazyk: stejný jako jazyk výrokové logiky; primárně používame systém spojek {=^, -i}, ostatní spojky jsou chápány jako zkrácené zápisy: A A B = B) A (fi A) • axiomy (resp. schémata axiomů; A, 6, C jsou formule): Ai A=>(B=>A) A2 (A=>(B=> C)) => {{A => B)^(A^ C)) A3 (-.6 -»4) (4 6) • odvozovací (inferenční) pravidlo modus ponens (MP) (pravidlo odloučení): jsou-li z axiomů dokazatelné (odvoditelné) formule A a A =>■ 6, pak je dokazatelná i 6. Zapisujeme též >A 4 => B B Úvod do umělé inteligence 7/12 7/51 • důkaz A: konečná posloupnost formulí, jejíž každý člen je axiom nebo důsledek MP, jehož předpoklady jsou mezi předchozími členy, a poslední člen je formule A. Je-li A dokazatelná, píšeme h A. • příklad: dokažte h A A (vpravo jsou komentáře k jednotlivým krokům) \.\- A=>{(A=> A)=> A) Ai 2. \-(A=> {(A ^A)^ A)) => {{A ^{A^ A)) => {A A)) A2 3. h (A (A A)) (A A) MP(1,2) 4. h A => (A A) Ai 5. \-A=>A MP(3,4) Úvod do umělé inteligence 7/12 8/51 Axiomatické systémy 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 • axiomy pro spojky (/4, 6, C jsou formule) - shodné s výr. logikou: Ai A^(B^A) 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 7/12 9/51 Axiomatické systémy Axiomatický systém predikátové logiky II • axiomy pro rovnost: A§ x = x A7 (* = y) . . . ,X/_i,X,X/+i, . . . ,X„) = f(xi,... ,x/_i,y,x/+i,... ,x„)) A8 (* = y) • • • ,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 /4 odvodíme MxA Úvod do umělé inteligence 7/12 10 / 51 Axiomatické systémy Axiomatický systém: příklad 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. \-A=>B předpoklad 2. hVx(4^e) PG(1) 3. h \/x{A B)=>(A=> Vx6) A5 4. h^^VxS MP(2,3) Úvod do umělé inteligence 7/12 11 / 51 Axiomatické systémy Vlastnosti axiomatického systému • Věta (korektnost a úplnost): A je dokazatelná právě tehdy, když je pravdivá, tj. h A ^ |= A Důkaz: =4> (korektnost): ověříme, že axiomy jsou tautologie a jsou-li předp. MP tautologie, pak i důsledek je tautologie (tabulky, věta o implikaci) (úplnost): složitější, na základě pomocných tvrzení (lemma o neutrální formuli a lemma o odvození z atomických komponent) Pozn.: věta vystihuje vztah mezi syntaxí a sémantikou výr. logiky 9 rozhodnutelnost: neexistuje systematická procedura (jde spíše o "hádánfjednotlivých kroků důkazu), nevhodné pro strojové zpracování. Dokazování lze zjednodušit pomocí dokazatelnosti z předpokladů a syntaktické věty o dedukci (7,/l h 8 T \- A ^ B). • axiomy jsou nezávislé (žádný nelze odvodit ze zbývajících dvou) Úvod do umělé inteligence 7/12 12 / 51 Axiomatické systémy 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) 9 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 7/12 13 / 51 Axiomatické systémy 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. hs(0) + s(0) = s(s(0)) PT(5,9) Úvod do umělé inteligence 7/12 14 / 51 Deduktivní systémy Deduktivní systémy Axiomatický systém je příkladem deduktivního systému (nebo též formálního systému). o postaveny výhradně na syntaktické bázi: jazyk logiky neinterpretujeme, provádíme s ním pouze syntaktické manipulace - důkazy • cíl: získat formální teorii jako souhrn dokazatelných formulí - teorémů • formální systém tvoří ■ jazyk + formule (symbolický jazyk výrokové logiky) - bez interpretací ■ odvozovací pravidla - operace na formulích umožňující konstrukce důkazů ■ případně axiomy - výchozí tvrzení přijímaná bez důkazu; (axiomy spolu s odvozovacími pravidly tvoří dedukční systém) • formální systémy lze rozdělit na ■ axiomatické (méně pravidel) ■ předpokladové (méně axiomů) Úvod do umělé inteligence 7/12 15 / 51 Deduktivní systémy Požadované vlastnosti formálních deduktivních systémů 9 (požadované) vlastnosti formálních (axiomatických) systémů: ■ korektnost (bezespornost): je dána výběrem axiomů a odvozovacích pravidel; systém je korektní, nelze-li v něm zároveň odvodit tvrzení i jeho negaci. Ve sporném systému lze odvodit cokoliv. Vyžadována vždy. (Sémantická korektnost: existuje alespoň jeden model.) ■ úplnost: připojením neodvoditelné věty k úplnému systému se tento stane sporným. Nevyžadována vždy - úplné jsou pouze velmi jednoduché teorie. (Sémantická úplnost: každé tvrzení pravdivé ve std. interpretaci lze odvodit.) ■ rozhodnutelnost: existence algoritmu pro ověření dokazatelnosti libovolné formule. V axiom, systémech podmíněna úplností; zpravidla splněna pouze pro určité třídy formulí. ■ nezávislost axiomů: nezávislý axiom nelze odvodit z ostatních axiomů; závislý axiom může být vypuštěn z dané soustavy axiomů Úvod do umělé inteligence 7/12 16 / 51 Rezoluce: další formální systém • vhodná pro strojové dokazování (Prolog) o metoda založená na vyvracení: dokazuje se nesplnitelnost formulí • pracujeme s formulemi v konjuktivní normální formě (též klauzulárním tvaru), ale používáme jinou notaci: o klauzule je konečná množina literálů (chápaná jako jejich disjunkce); je pravdivá, pokud alespoň jeden prvek je pravdivý. Prázdná klauzule □ je vždy nepravdivá - neobsahuje žádný pravdivý prvek. Příklad klauzule: {p, -iq, r} (tj. p V -iq V r) • formule je (ne nutně konečná) množina klauzulí (chápaná jako jejich konjunkce, tedy nkf); je pravdivá, je-li každý prvek pravdivý. Prázdná formule 0 je vždy pravdivá - neobsahuje žádný nepravdivý prvek. Příklad formule: {{-q}, {--p, q], {p, q, r}} (tj. -■q A (-ip V q) A (p V q V r)) Úvod do umělé inteligence 7/12 17 / 51 • rezoluční pravidlo: nechť C\ — {p} U C{, C2 = {^p} U C2 jsou klauzule, jejich rezolventou je C = C[ U C^ (rezolvovali jsme na literálu p) a rezoluční pravidlo zachovává splnitelnost (lib. valuace splňující C\ a C2 splňuje i C; klauzule Ci, C2 označujeme jako rodiče, C jako potomka) • rezoluční důkaz klauzule C z formule S je konečná posloupnost klauzulí Ci, C2,..., C„, kde Cn = Ca každé C; je buď prvkem S, nebo rezolventou klauzulí Cy, Q pro j, /c < /. Existuje-li tento důkaz, je C rezolučně dokazatelná z S (píšeme S \-r C). Odvození □ z S je vyvrácením S. o příklad: dokažte C = {^q} z S = {{p, r}, {^q, -ir}, {^p}} Ci = {p, r} (prvek S), C2 = {^q, ^r} (prvek S), C3 = {p, ^q} (rezolventa Ci, C2), C4 = {^p} (prvek S), C = C5 = {^q} (rezolventa C3, C4) Úvod do umělé inteligence 7/12 18 / 51 Rezoluce - stromy Rezoluční metoda přehlednější formou rezolučních důkazů jsou stromy • strom rezolučního důkazu C z S je binární strom T s vlastnostmi: ■ kořenem T je C ■ listy T jsou prvky S ■ libovolný vnitřní uzel C, s bezprostředními následníky Cý, Ck je rezolventou Cj, Ck o příklad: strom důkazu C = {^q} z S = {{p, r}, {^q, -"r}, {^p}} Úvod do umělé inteligence 7/12 19 / 51 Rezol uce - stromy Rezoluční metoda přehlednější formou rezolučních důkazů jsou stromy • strom rezolučního důkazu C z S je binární strom T s vlastnostmi: ■ kořenem T je C ■ listy T jsou prvky S ■ libovolný vnitřní uzel C, s bezprostředními následníky Cý, Ck je rezolventou Cj, Ck o příklad: strom důkazu C = {^q} z S = {{p, r}, {^q, -"r}, {^p}} Úvod do umělé inteligence 7/12 20 / 51 Rezoluční metoda Příklad: Rezoluční vyvrácení příklad: vytvořte strom rezolučního vyvrácení S (dokažte S \-r □), je-li S = {{p, r}, {q, -.r}, {-g}, {^p, t}, {^s}, {s, ^t}} Úvod do umělé inteligence 7/12 21 / 51 Rezoluční metoda Rezoluce - vlastnosti • Věta (korektnost a úplnost rezoluce): rezoluční vyvrácení formule S existuje právě tehdy, když je S nesplnitelná. • důsledek: existuje-li rezoluční strom s listy z množiny S a kořenem □, pak je S nesplnitelná • obecné schéma důkazu "formule A je log. důsledkem množiny formulí T": vytvoříme konjunkci Tr všech prvků z T, formuli Tr A -iA převedeme do nkf a ukážeme nkf(7; A ^A) \-r □ • výhody pro strojové zpracování: systematické hledání důkazu, práce s jednoduchou datovou strukturou, jediné odvozovací pravidlo o problém: strategie generování rezolvent - prohledávaný prostor může být příliš velký; př.: {{p}, {p, ^q}, {^p, q, r}, {^p, ^r}, {r}} - postup, kdy rezolvujeme 2. a 3. klauzuli na p a výsledek poté se 4. na r, k důkazu nevede Úvod do umělé inteligence 7/12 22 / 51 Rezoluční metoda Zjemnění rezoluce • snaha omezit prohledávaný prostor ■ ukončením prohledávání neperspektivních cest ■ určením pořadí při procházení alternativních cest • = další podmínky na rodičovské klauzule nebo rezolventu v definici rezoluce • každé omezení rezolučního pravidla je korektní, ne každé zachovává úplnost. Příklady možných zjemnění • vyloučení klauzulí s literálem, který je ve formuli S pouze v jedné paritě • T-rezoluce: žádná z rodičovských klauzulí není tautologie, tautologie obsahuje týž literál v obou paritách např. {p, -iq, -ip, r} • nechť A je libovolná interpretace, ^4-rezoluce (sémantická rezoluce) je rezoluce, kde alespoň jedna z rodičovských klauzulí je v A nepravdivá. (Budou-li rodiče v dané valuaci pravdiví, bude v ní pravdivý i potomek - touto cestou k nesplnitelnosti nedojdeme, yl-rezoluce je korektní a úplná.) Úvod do umělé inteligence 7/12 23 / 51 Rezoluční metoda Unifikace - motivace směřujeme k rezoluci v predikátové logice: ■ formule umíme reprezentovat v konjunktivní pnf odpovídající klauzulární formě (V nepíšeme, ale předpokládáme univerzální kvantifikaci všech proměnných) ■ literály nyní představují atomické formule a jejich negace ■ zůstává jediný problém: jak instanciovat proměnné, aby bylo možné použít rezoluční pravidlo • příklad: mějme klauzule C\ — {P(ŕ(x)),-i(?(a,x)} a C2 = {^P(f(g(a)))}\ nahradíme-li x termem g"(a), získáme rezolventu {^Q(a,g(a))} poznámka: C\ odpovídá formuli Vx(P(/ľ(x)) V ^Q(a, x)), takže můžeme použít libovolnou instanci o obecně řeší uvedený problém se substitucemi proměnných unifikace Úvod do umělé inteligence 7/12 24 / 51 Substituce Rezoluční metoda • konečná substituce cf) je konečná množina {xi/ti, x^jt^..., xn/tn}, kde všechna x; jsou vzájemně různé proměnné a každé ŕ; je term různý od x/. Jsou-li všechna ŕ; uzavřené termy, jedná se o uzavřenou substituci. Pokud jsou ti proměnné, označujeme (f) jako přejmenování proměnných. • označme libovolný term nebo literál jako výraz E; pak Ecf) je výsledek nahrazení všech výskytů všech x; odpovídajícími termy ŕ; (obdobně pro množiny výrazů) poznámka: substituce proměnných probíhají paralelně, ne postupně příklad: S = {f(x, g(y)), -P(y, x), Q(y, z, a)} 0={x//I(y),y/g(z),z/c} S0 = {f(h(y),g(g(z))), -P(g(z), %)), (?fjr(z), c, a)} Úvod do umělé inteligence 7/12 25 / 51 Rezoluční metoda Kompozice substitucí o kompozice substitucí (f) = {xi/ti,... ,xn/tn} aijj = {yi/si,... ,y™/sm} je množina 0^ = {xi/hý, • • • ,xn/tný,yi/si,... ,ym/sm} beze všech x;/^, pro která x; = t,-^, a všech yj/sj^yj £ {xi,... ,xn} • pro prázdnou substituci e a libovolnou substituci (/) platí 0e = ecj) = 0 • pro libovolný výraz E a substituce (j),ip,(J platí (E(/))íp = E(cf)ip) a příklad: 5 = {f (x, g(y)), -P(y, x), (?(y, z, a)} 0 = {x//j(y),y/w,z/g(w,y)}, V = {x/a,y/f(í>), w/y} 0^ = {x//j(/r(6)),z/á:(y,r(6)),M//y} S0={r(/7(y),ár(M/)),-P(M/,/7(y)),(?(M/,ár(M/,y),a)} S(0VO = (S0)V = {f(/i(f(£>)),fir(y)), -P(y, = E2(j) = • • • = 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(b, c)}, {P(f(x), z), P(a, {P(x, -.P(a, w)}, {P(x,y, z), P(a, fo)}, {/?(x), P(x)} nejsou unifikovatelné 2. unifikátorem {P(x, c), P(b, c)} je = {x/fo}; žádný jiný neexistuje 3. unifikátorem {P(f(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/b, atd. • unifikátor

),s(a)), h(b)), P(f(h(b),g(a)),xl P(f(h(b),g(a)), h(b))} 4. D(S3) = {b(b),x},4 = {x//7(b)},S4 = S304 = {P(f(b(b),g(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 7/12 30 / 51 Rezoluce v predikátové logice 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 (-.P(f(x)) V ->(?(y))) reprezentujeme jako {{P(x, f (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 7/12 31 / 51 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 I V S I V S I / \f / I s v ■ x x\ . společných proměnných (po pripadnem přejmenovaní) ve tvaru Ci = C[ U {P(xi),..., P(x„)}, C2 = C£ U {-P(ýi),..., -iP(ym)}. Je-N 0 mgu množiny {P(j?i),..., P(x„), P(ýi)j • • • 5 P(ým)}. pak rezolventou Ci a C2 je C(0 U C^cf). • 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 7/12 32 / 51 Rezoluce v predikátové logice Rezolventa - příklady I 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)} • mgu({P(x,y),P(a,b)}) = {x/a,y/b} o aplikujeme mgu na {^P(x)} • rezolventa {^P(a)} Úvod do umělé inteligence 7/12 33 / 51 Rezoluce v f: )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(f (a), f (a)), -P(r», f(w))} • 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))} 9 její mgu 0 = {x/f(a),y/f(a),z/a, w/a] • C[ = {(?(x),--/?(/)}, CÍ0 = {(?(f(a)),-./?(f(a))} • C2 = {^N{u),^R{w)}, C24> = {^N{u),^R{a)} 9 výsledná rezolventa C[0U C24> = {Q(f(a)),^R(f(a)),^N(u),^R(a)} Úvod do umělé inteligence 7/12 34 / 51 Rezoluce v predikátové logice Rezoluční důkazy 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(Xl)^P(yi)} □ Úvod do umělé inteligence 7/12 35 / 51 Rezoluce v predikátové logice Rezoluční důkaz - příklad I Z předpokladu reflexivity VxP(x,x) a vlastnosti VxVyVz((P(x,y) A P(y,z)) => P(z,x)) dokažte symetrii \/xVy(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)}} • 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 7/12 36 / 51 Rezoluce v predikátové logice Rezoluční důkaz - příklad II 9 dokazujeme nesplnitelnost množiny klauzulí {{P(x, x)}, {-P(x,y), -nP(y, z), P(z, x)}, {P(a, />)}, {-P(f>, a)}} » strom rezolučního vyvrácení (jeden z možných): {-PO, y), -P(y, z),P(z, a;)} {P(a, 6)} Úvod do umělé inteligence 7/12 37 / 51 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) 9 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 7/12 38 / 51 • 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 ■ • príklad: lineárni rezoluční vyvraceni množiny {{P(x, x)}, {-P(x,y), -nP(y, z), P(z, x)}, {P(a, />)}, {-P(f>, a)}} {-PO, 3,), -iP(y, z), P(z, x)} {P(a, b)} x/a,y/b x/a,y/b {^P(b,z),P(z,a)} {-.P(6,o)} {-P(M)} {P(x,x)} s/6 as/fa Úvod do umělé inteligence 7/12 39 / 51 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. o 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 7/12 40 / 51 • 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 o pracujeme výhradně s Hornovými klauzulemi (nejvýše jeden pozitivní literál) 9 klauzule nahradíme uspořádanými klauzulemi; změna notace z {P(x),^R(x,f(y)),^Q(3)} na [P(x), -P(x, f{y)), -n ^q} {p> q} {^p, q} ÍPi ^q} i^P; q} Úvod do umělé inteligence 7/12 42 / 51 • LD-rezoluční vyvrácení množiny uspořádaných klauzulí {[P(x, x)}, [P(z, x), -P(x, y), -P(y, z)], [P(a, b)], [-^P(b, a)]} [-.P(M] [P^iJ.-.P^yJ.-.PÍj/.z)] xj a,z jb [^P{a,y)^P(yM [P(o, 6)] hP(a,a)] [P(i,i)] □ Úvod do umělé inteligence 7/12 43 / 51 SLD-rezoluce Rezoluce v predikátové logice • pomocí selekčního pravidla algoritmizuje výběr literálu z cílové klauzule, na kterém se bude rezolvovat a 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,..., -»An0] Úvod do umělé inteligence 7/12 44 / 51 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(y}z)} x ja,z/b bP(aty)t^P(y,b)] [P(a,b)} 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 7/12 45 / 51 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)) o uvedená nesplnitelnost je ekvivalentní P I—iG, tj. Ph3x(^i(x)A... AAn(x)) • 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 7/12 46 / 51 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,y),^Q(x,z),^R(z,y)] 2. [P(x,x),^S(x)] 3. ÍQ(x,b)] 4. [Q(b,a)] 5. [S(x)] 8 R{b,x)} [->R{a,b)][->R{a,x),R(a,x)] hT(z,a)] hT(z,č>)] [->T(x,x)] 6 D[x/a] neúspěch neúspěch 11 10 a [x/b] a[x/a] neúspěch Úvod do umělé inteligence 7/12 48 / 51 Logické programovaní Logické programovaní • strategie prohledávání stavového prostoru (SLD-stromu) do hloubky • výběr programových klauzulí shora dolů • výběr podcílů zleva doprava (viz selekční pravidlo v SLD rezoluci) 9 silně využívá rekurzi • historie: 70. I. 20. stol. - Colmerauer, Kowalski; D.H.D. Warren (WAM) • jazyk Prolog Úvod do umělé inteligence 7/12 49 / 51 Logické programovaní SLD-odvození pro logic ký 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)) num(s(X)), —i num(X) Úvod do umělé inteligence 7/12 50 / 51 Logické programovaní Příklad: Sčítaní dvou čísel x + Y = z VX : X + 0 = X VXVVVZ : 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 7/12 51 / 51