Rezoluce v predikátové logice I. řádu (pokračování) Rezoluční princip ve výrokové logice ■ Rezoluční princip = pravidlo, které umožňuje odvodit z klauzulí d u {1} a {-ii} u Cz klauzuli C\ u Cz Ciujil HluC2 QuC2 ■ 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é - je pravdivý alespoň jeden z jejích literálů ■ prázdná klauzule se značí □ a je 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: (pvij)A (->p) a (p v -iq v r) notace: {{p,q}, {->p}, {p, -^,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, 5. dubna 2012 2 Rezoluce v PL1 Rezoluční důkaz ■ rezoluční důkaz klauzule C z formule F je konečná posloupnost Ci,..., Cn = C klauzulí taková, že Q je buď klauzule z F nebo rezolventa C,, Ct pro k,j < í. ■ příklad: rezoluční důkaz {p} z formule F = {{p,r}, {q, - 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, 5. dubna 2012 5 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, 5. dubna 2012 6 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(W), ->p(f(W),f(W)} Hana Rudová, Logické programování I, 5. dubna 2012 7 Rezoluce v PL1 Hana Rudová, Logické programování I, 5. dubna 2012 8 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, 5. dubna 2012 9 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, 5. dubna 2012 10 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} HTi.....^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, 5. dubna 201 2 15 Rezoluce a logické programování Hana Rudová, Logické programování I, 5. dubna 2012 14 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, 5. dubna 2012 16 Rezoluce a logické programování Lineární rezoluce pro Hornovy klauzule Lineární vstupní rezoluce 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>} (pJ {^ql lil \/ \/ □ □ Střední klauzule jsou cílové klauzule Hana Rudová, Logické programování I, 5. dubna 201 2 Rezoluce a logické programování 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 P je posloupnost dvojic (C0,Bo>, ■ ■ ■ (Cn,Bn) taková, že C = Cn+i a ■ Q a každá i?; jsou prvky P 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, 5. dubna 2012 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, 5. dubna 201 2 1 9 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 = ÍPl.....Pn], G = {Gl.....Gm\ ■ Ll-rezolucí ukážeme nesplnitelnost P\ a ■ ■ ■ a Pn a (-iGi v ■ ■ ■ v -iGm) ■ 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, 5. dubna 2012 20 Rezoluce a logické programování Uspořádané klauzule (definite clauses) Klauzule = množina literálů Uspořádaná klauzule (definite cl a use) = posloupnost literálů ■ nelze volně měnit pořadí literálů Rezoluční princip pro uspořádané klauzule: Í^A0.....^4„} {ď,-.ď0, ...,-.£,„} \^Ap.....-'Aí-i, -^Bop,-^Bmp, ->Ai+i,-iA„}cr ■ uspořádaná rezolventa: {-