Rezoluce Rezoluce v predikátové logice l.řá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) ■ ti, ■ ■ ■ , t„jsou termy 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, 26. března 2013 3 Rezoluce v PL1 Hana Rudová, Logické programování I, 26. března 2013 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\. D = 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, 26. března 2013 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 G = ^F...a a -ia G = ->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, 26. března 2013 7 Rezoluce v PL1 Hana Rudová, Logické programování I, 26. března 201 3 Rezoluce v PL1 Strom rezolučního důkazu ■ strom rezolučního důkazu klauzule C z formule G je binární strom: ■ kořen je označen klauzulí C, ■ listy jsou označeny klauzulemi z G 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: G = {{p,r}, {q, -ir}, {-*q}, {^p}} C = D {p,r} {q,^r} {^q} {^p} strom rezolučního vyvrácení (rezoluční důkaz □ z G) příklad: {{p,r}, {q, ^r}, {^q}, {^p, t}, {^s}, {s, ^ŕ}} Hana Rudová, Logické programování I, 26. března 201 3 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, 26. března 2013 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, 26. března 2013 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(W), ->p(f(W),f(W)} Hana Rudová, Logické programování I, 26. března 2013 11 Rezoluce v PL1 Hana Rudová, Logické programování I, 26. března 2013 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, 26. března 2013 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, 26. března 2013 14 Rezoluce v