Rezoluce Rezoluce v predikátové logice I. řádu ■ rezoluční princip: z F v A, G v ->A odvodit F v G ■ dokazovací metoda používaná ■ v Prologu ■ ve většině systémů pro automatické dokazování ■ procedura pro vyvrácení ■ hledáme důkaz pro negaci formule ■ snažíme se dokázat, že negace formule je nesplnitelná => formule je vždy pravdivá Formule literál / ■ pozitivní literál = atomická formule p(h, ■ ■ ■ ,tn) ■ negativní literál = negace atomické formule ->p(t\, ■ ■ ■ ,tn) klauzule C = konečná množina literálů reprezentující jejich disjunkci ■ příklad: p(X) v q(a,f) v -ip(Y) notace: {p(X),q(a,f),-ip(Y)} ■ klauzule je pravdivá je pravdivý alespoň jeden z jejích literálů ■ prázdná klauzule se značí □ aje vždy nepravdivá (neexistuje v ní pravdivý literál) formule F = množina klauzulí reprezentující jejich konjunkci ■ formule je v tzv. konjuktivní normální formě (konjunkce disjunkcí) ■ příklad: (p v q) a (-ip) a (p v -iq v r) notace: {{p,q}, {->p}, {p, -^q,r}} ■ formule je pravdivá <=> všechny klauzule jsou pravdivé ■ prázdná formule je vždy pravdivá (neexistuje klauzule, která by byla nepravdivá) množinová notace: literál je prvek klauzule, klauzule je prvek formule, ... Hana Rudová, Logické programování I, 7. dubna 2009 3 Rezoluce v PL1 Hana Rudová, Logické programování I, 7. dubna 2009 2 Rezoluce v PL1 Splnitelnost ■ [Opakování:] Interpretace 1 jazyka L je dána univerzem T> a zobrazením, které přiřadí konstantě c prvek T>, funkčnímu symbolu f In n-ární operaci v T> a predikátovému symbolu p In n-ární relaci. ■ příklad: F = {{f(a,b)=f(b,a)}, {f(f(a,a),b) = a}} interpretace 1\. T> = Z,a := l,b := -1,/ := " + " ■ Formule je splnitelná, existuje-li interpretace, pro kterou je pravdivá ■ formule je konjunkce klauzulí, tj. všechny klauzule musí být v dané interpretaci pravdivé ■ příklad (pokrač.): F je splnitelná (je pravdivá v 'h) ■ Formule je nesplnitelná, neexistuje-li interpretace, pro kterou je pravdivá ■ tj. formule je ve všech iterpretacích nepravdivá ■ tj. neexistuje interpretace, ve které by byly všechny klauzule pravdivé ■ příklad: G = {{p(b)}, {p(a)}, {->p(«)}} je nesplnitelná ({p(a)\ a {-ip(a)} nemohou být zároveň pravdivé) Hana Rudová, Logické programování I, 7. dubna 2009 4 Rezoluce v PL1 Rezoluční princip ve výrokové logice Rezoluční důkaz Rezoluční princip = pravidlo, které umožňuje odvodit z klauzulí d u {1} a {-ii} u C2 klauzuli C\ u C2 Ciujil HluC2 CiuC2 Ci u C2 se nazývá rezolventou původních klauzulí příklad: {p,r} {^r,s} (p v r) a (-if v í) {p,s} p v s obě klauzule (pvr)a (-ir v 5) musí být pravdivé protože r nestačí k pravdivosti obou klauzulí, musí být pravdivé p (pokud je pravdivé - -iF je nepravdivá ve všech interpretacích => F je vždy pravdivá začneme-li z klauzulí reprezentujících -if, musíme postupným uplatňováním rezolučního principu dospět k prázdné klauzuli □ Příklad: F ... -ifl v a -i F ... a a -ifl -■F ... {{a}, {-"a}} Ci = {fl},C2 = {-ia} rezolventa C\ a C2 je □, tj. F je vždy pravdivá rezoluční důkaz □ z formule G se nazývá rezoluční vyvrácení formule G ■ a tedy C je nepravdivá ve všech interpretacích, tj. C je nesplnitelná Hana Rudová, Logické programování I, 7. dubna 2009 7 Rezoluce v PL1 Hana Rudová, Logické programování I, 7. dubna 2009 Rezoluce v PL1 Strom rezolučního důkazu ■ strom rezolučního důkazu klauzule C z formule F je binární strom: ■ kořen je označen klauzulí C, ■ listy jsou označeny klauzulemi z F a ■ každý uzel, který není listem, ■ má bezprostředními potomky označené klauzulemi Q a C2 ■ je označen rezolventou klauzulí C\ a Ci ■ příklad: F = {{p,r}, {q, -*r}, {^q}, {^p}} C = U {p,r} {q,^r} {^q} {^p} strom rezolučního vyvrácení (rezoluční důkaz □ z F) příklad: {{p,r}, {q, ^r}, {^q}, {^p, t}, {^s}, {s, ^ŕ}} Hana Rudová, Logické programování I, 7. dubna 2009 Rezoluce v PLI Substituce co s proměnnými? vhodná substituce a unifikace ■ f(X,a,g(Y)) < l,f(h(c),a,Z) < 1, X = h(c), Z = g(Y) => f(h(c), a,g(Y)) < 1 substituce je libovolná funkce 9 zobrazující výrazy do výrazů tak, že platí ■ 6(E) = E pro libovolnou konstantu E ■ 0(f(Ei, ■ ■ ■ ,£„)) = f (9(Ei), ■ ■ ■ , 0(En)) pro libovolný funkční symbol / ■ 0(p(Ei, ■ ■ ■ ,En)) = p(0(Ei), ■ ■ ■ , 9(En)) pro libovolný predik. symbol p substituce je tedy homomorfismus výrazů, který zachová vše kromě proměnných - ty lze nahradit čímkoliv substituce zapisujeme zpravidla ve tvaru seznamu [Xi/gi, ■ ■ ■ ,Xn/%n] kde Xi jsou proměnné a substituované termy ■příklad: p(X)[X/f(a)] = p(f(a)) přejmenování proměnných: speciální náhrada proměnných proměnnými ■příklad: p(X)[X/Y] = p(Y) Hana Rudová, Logické programování I, 7. dubna 2009 9 Rezoluce v PL1 Unifikace ■ Ztotožnění dvou literálů p, q pomocí vhodné substituce a takové, že pa = qa nazýváme unifikací a příslušnou substituci unifikátorem. ■ Unifikátorem množiny S literálů nazýváme substituce 9 takovou, že množina S9 = {te\t e S} má jediný prvek. ■ příklad: S = { datum( Dl, Ml, 2003 ), datum( 1, M2, Y2) } unifikátor 6 = [Dl/l, Ml/2, M2/2, Y2/2003] S0 = { datum( 1, 2, 2003 ) } ■ Unifikátor a množiny S nazýváme nejobecnějším unifikátorem (mgu - most generál unifier), jestliže pro libovolný unifikátor 9 existuje substituce A taková, že 9 = crA. ■ příklad (pokrač.): nejobecnější unifikátor a = [Dl /l, Y2/2003, Ml /M2], A=[M2/2] Hana Rudová, Logické programování I, 7. dubna 2009 10 Rezoluce v PL1 Rezoluční princip v PL1 základ: ....... . . . Q u {i} HluC2 ■ rezoluční princip ve výrokové logice -—-—- Ci u c2 ■ substituce, unifikátor, nejobecnější unifikátor rezoluční princip v PL1 je pravidlo, které ■ připraví příležitost pro uplatnění vlastního rezolučního pravidla nalezením vhodného unifikátoru ■ provede rezoluci a získá rezolventu Ci u {A} {^B}uC2 C\pu u C2cr ■ kde p je přejmenováním proměnných takové, že klauzule (C\ uA)p a {B} u C2 nemají společné proměnné ■ cr je nejobecnější unifikátor klauzulí Ap a B Příklad: rezoluce v PL1 ■ příklad: d = {p(X,Y), q(Y)} C2 = {^q(a), s(X,W)} ■ přejmenování proměnných: p = [XIZ] Ci = {p(Z,Y), q(Y)} C2 = {^q(a), s(X,W)} ■ nejobecnější unifikátor: a = [Y/a] Ci = {p(Z,a), q(a)} C2 = {^q(a), s(X,W)} ■ rezoluční princip: C = {p(Z, a), s(X, W)} ■ vyzkoušejte si: d = {q(X), -.r(y), p(X,Y), p(/(Z),/(Z))} C2 = {n(Y), -.r(^), -.p(/(a),/(a)), ^p(f(W),f(W)} Hana Rudová, Logické programování I, 7. dubna 2009 11 Rezoluce v PL1 Hana Rudová, Logické programování I, 7. dubna 2009 12 Rezoluce v PL1 Rezoluce v PLI Obecný rezoluční princip v PL1 Ciu{4-Al {-.ďi,-■-,-.£„} uC2 C\pu u C20" ■ kde p je přejmenováním proměnných takové, že množiny klauzulí {A\p, ■ ■ ■ ,Amp, C\p} a {Bi, ■ ■ ■ ,Bn, C2} nemají společné proměnné ■ crje nejobecnější unifikátor množiny {A\p, ■ ■ ■ ,Amp,B\, ■ ■ ■ ,Bn} ■ příklad: Ai = a(X) vs. {-1B1, -iB2] = {^a(b),^a(Z)} v jednom kroku potřebuji vyrezolvovat zároveň Bi i B2 Rezoluce v PL1 ■ korektní: jestliže existuje rezoluční vyvrácení F, pak F je nesplnitelná ■ úplná: jestliže F je nesplnitelná, pak existuje rezoluční vyvrácení f Hana Rudová, Logické programování I, 7. dubna 2009 13 Rezoluce v PL1 Varianty rezoluční metody Věta: Každé omezení rezoluce je korektní. ■ stále víme, že to, co jsme dokázali, platí T-rezoluce: klauzule účastnící se rezoluce nejsou tautologie úplná ■ tautologie nepomůže ukázat, že formule je nesplnitelná sémantická rezoluce: úplná zvolíme libovolnou interpretaci a pro rezoluci používáme jen takové klauzule, z nichž alespoň jedna je v této interpretaci nepravdivá ■ pokud jsou obě klauzule pravdivé, těžko odvodíme nesplnitelnost formule vstupní (input) rezoluce: neúplná alespoň jedna z klauzulí, použitá při rezoluci, je z výchozí vstupní množiny S " {{p,í?}, í-'P.q.}, {p,"■ varianty rezoluční metody ■ vylepšení prohledávání ■ zastavit prohledávání cest, které nejsou slibné ■ specifikace pořadí, jak procházíme alternativními cestami Hana Rudová, Logické programování I, 7. dubna 2009 14 Rezoluce v Rezoluce a logické programování Lineární rezoluce Lineární rezoluce II. varianta rezoluční metody ■ snaha o generování lineární posloupnosti místo stromu ■ v každém kroku kromě prvního můžeme použít bezprostředně předcházející rezolventu a k tomu buď některou z klauzulí vstupní množiny S nebo některou z předcházejících rezolvent lineární rezoluční důkaz C z S je posloupnost dvojic , ■ ■ ■ {Cn,Bn) taková, že C = Cn+i a ■ Co a každá Bi jsou prvky S nebo některé Cj.j < i ■ každá Ci+i, i < n je rezolventa Q a Bi lineární vyvrácení S = lineární rezoluční důkaz □ z S C, C příklad: 5 = {Ax, A2, A3, A4] Ai = {p,q} A2 = {p, -*q} Aj, = {^p.q} A4 = {^p, -^q] S: vstupní množina klauzulí (',: střední klauzule Bc boční klauzule C i Bi {p,q}{p, -iq} \/ (pJ l^p,q} \/ lq} {~TU ■ ■ ■ , -.r„} Hi v ■ ■ ■ v Hm v -iTi v ■■■ v -iTu Hornova klauzule: nejvýše jeden pozitivní literál ' {H.^Ti.....^T„} {H} {^Ti.....^T„} ■ H v -iTi v ■ ■ ■ v ->Tn H -iTi v ■ ■ ■ v ->Tn Pravidlo: jeden pozitivní a alespoň jeden negativní literál ■ Prolog: H : - Ti, ■ ■ ■ ,Tn. Matematická logika: H <= Ti a ■ ■ ■ a Tn ■H^T H v-.T H v -.Ti v ■ ■ ■ v -iTn Klauzule: {H,-.Ti.....-iTn] Fakt: pouze jeden pozitivní literál ■ Prolog: H. Matematická logika: H Klauzule: {H} Cílová klauzule: žádný pozitivní literál ■ Prolog: : - Ti,... Tn. Matematická logika: -iTi v ■ ■ ■ v -iTn Klauzule: {-iTi, ■ ■ ■ ->Tn} Hana Rudová, Logické programování I, 7. dubna 2009 19 Rezoluce a logické programování Hana Rudová, Logické programování I, 7. dubna 2009 1 8 Rezoluce a logické programování Logický program ■ Programová klauzule: právě jeden pozitivní literál (fakt nebo pravidlo) ■ Logický program: konečná množina programových klauzulí ■ Příklad: ■ logický program jako množina klauzulí: P = {P1.P2.p3} Pi = {p], Pz = {p,^q}, P3={q] ■ logický program v prologovské notaci: V- v ■ -a- q. ■ cílová klauzule: G = {^q, -^p} : -q, p. Hana Rudová, Logické programování I, 7. dubna 2009 20 Rezoluce a logické programování Lineární rezoluce pro Hornovy klauzule Začneme s cílovou klauzulí: Co = G Boční klauzule vybíráme z programových klauzulí P G={^q,^p} P={P1,P2,P3}: Pi = {p), P2 = iP,^q}, P3 = iq) :-q,p. p. P--q, q. {^q,^p} Iq} \/, , \/ \/ {-i>} fal {^ql fa} \/ \/ □ □ Střední klauzule jsou cílové klauzule Hana Rudová, Logické programování I, 7. dubna 2009 Rezoluce a logické programování Lineární vstupní rezoluce Vstupní rezoluce na P u {G} ■ (opakování:) alespoň jedna z klauzulí použitá při rezoluci je z výchozí vstupní množiny ■ začneme s cílovou klauzulí: Co = G ■ boční klauzule jsou vždy z P (tj. jsou to programové klauzule) (Opakování:) Lineární rezoluční důkaz C z S je posloupnost dvojic (Co, Bo), ■ ■ ■ (Cn,Bn) taková, že C = Cn+i a ■ Q a každá Bí jsou prvky S nebo některé Cj,j < í ■ každá Cí+i, í < n je rezolventa C; a Bí Lineární vstupní (Linear ínput) rezoluce (Ll-rezoluce) C z P u {G} posloupnost dvojic (Co,Bo), ■ ■ ■ (Cn,Bn) taková, že C = Cn+\ a ■ Co = G a každá Bi JSOU prvky P lineární rezoluce + vstupní rezoluce ■ každá Cf+i, i < n je rezolventa Q a Bí Hana Rudová, Logické programování I, 7. dubna 2009 Rezoluce a logické programování Cíle a fakta při lineární rezoluci ■ Věta: Je-li S nesplnitelná množina Hornových klauzulí, pak S obsahuje alespoň jeden cíl a jeden fakt. ■ pokud nepoužiji cíl, mám pouze fakta (1 požit.literál) a pravidla (1 požit.literál a alespoň jeden negat. literál), při rezoluci mi stále zůstává alespoň jeden požit, literál ■ pokud nepoužiji fakt, mám pouze cíle (negat.literály) a pravidla (1 požit.literál a alespoň jeden negat. literál), v rezolventě mi stále zůstávají negativní literály ■ Věta: Existuje-li rezoluční důkaz prázdné množiny z množiny S Hornových klauzulí, pak tento rezoluční strom má v listech jedinou cílovou klauzuli. ■ pokud začnu důkaz pravidlem a faktem, pak dostanu zase pravidlo ■ pokud začnu důkaz dvěma pravidly, pak dostanu zase pravidlo ■ na dvou faktech rezolvovat nelze => dokud nepoužiji cíl pracuji stále s množinou faktů a pravidel ■ pokud použiji v důkazu cílovou klauzulí, fakta mi ubírají negat.literály, pravidla mi je přidávají, v rezolventě mám stále samé negativní literály, tj. nelze rezolvovat s dalším cílem Hana Rudová, Logické programování I, 7. dubna 2009 23 Rezoluce a logické programování Korektnost a úplnost ■ Věta: Množina S Hornových klauzulí je nesplnitelná, právě když existuje rezoluční vyvrácení S pomocí vstupní rezoluce. ■ Korektnost platí stejně jako pro ostatní omezení rezoluce ■ Úplnost Ll-rezoluce pro Hornovy klauzule: Nechť P je množina programových klauzulí a G cílová klauzule. Je-li množina P u {G} Hornových klauzulí nesplnitelná, pak existuje rezoluční vyvrácení P u {G} pomocí Ll-rezoluce. ■ vstupní rezoluce pro (obecnou) formuli sama o sobě není úplná => Ll-rezoluce aplikovaná na (obecnou) formuli nezaručuje, že nalezeneme důkaz, i když formule platí! ■ Význam Ll-rezoluce pro Hornovy klauzule: ■ P = ÍPi.....Pn), G = {Gi.....Gm] ■ Ll-rezolucí ukážeme nesplnitelnost P\ a ■ ■ ■ a Pn a (-iGi v ■ ■ ■ v ^Gm) ■ pokud tedy předpokládáme, že program {Pi.....Pn\ platí, tak musí být nepravdivá (-iGi v ■ ■ ■ v -iGm), tj. musí platit Gi a ■ ■ ■ a Gm Hana Rudová, Logické programování I, 7. dubna 2009 24 Rezoluce a logické programování