Rezoluce v predikátové logice I. řádu (pokračování) Formule Ji literal l & pozitivní literal = atomická formule p(t1, • • • ,tn) &> negativní literal = negace atomické formule -p(ti, • • • ,tn) Hana Rudová, Logické programování I, 5. dubna 2012 2 Rezoluce v PL1 Formule Ji literál l -fc pozitivní literál = atomická formule p(t1, • • • ,tn) &> negativní literál = negace atomické formule —p(t1, • • • ,tn) klauzule C = koneCná množina literálů reprezentující jejich disjunkci príklad: p(X) v q(a,f) v -p(Y) notace: {p(X),q(a, f),-p(Y)} -i- klauzule je pravdivá <=> je pravdivý alespoň jeden z jejích literálů -í* prázdná klauzule se znací □ a je vždy nepravdivá (neexistuje v ní pravdivý literál) Hana Rudová, Logické programování I, 5. dubna 2012 2 Rezoluce v PL1 Formule Ji literál l -fc pozitivní literál = atomická formule p(t1, • • • ,tn) &> negativní literál = negace atomické formule —p(t1, • • • ,tn) klauzule C = koneCná množina literálů reprezentující jejich disjunkci príklad: p(X) v q(a,f) v -p(Y) notace: {p (X), q(a, f),-p(Y)} -i- klauzule je pravdivá <=> je pravdivý alespoň jeden z jejích literálů -í* prázdná klauzule se znací □ a je vždy nepravdivá (neexistuje v ní pravdivý literál) -í* formule F = množina klauzulí reprezentující jejich konjunkci a formule je v tzv. konjuktivní normální forme (konjunkce disjunkcí) i> príklad: (p v q) a (-p) a (p v-q v r) notace: {{p, q}, {-p}, {p, -q,r}} Hana Rudová, Logické programování I, 5. dubna 2012 2 Rezoluce v PL1 Formule Ji literál l -fc pozitivní literál = atomická formule p(t1, • • • ,tn) &> negativní literál = negace atomické formule —p(t1, • • • ,tn) klauzule C = koneCná množina literálů reprezentující jejich disjunkci príklad: p(X) v q(a,f) v -p(Y) notace: {p (X), q(a, f),-p(Y)} -i- klauzule je pravdivá <=> je pravdivý alespoň jeden z jejích literálů -í* prázdná klauzule se znací □ a je vždy nepravdivá (neexistuje v ní pravdivý literál) -í* formule F = množina klauzulí reprezentující jejich konjunkci A formule je v tzv. konjuktivní normální forme (konjunkce disjunkcí) i> príklad: (p v q) a (-p) a (p v-q v r) notace: {{p, q}, {-p}, {p, -q,r}} A formule je pravdivá <=> všechny klauzule jsou pravdivé J> prázdná formule je vždy pravdivá (neexistuje klauzule, která by byla nepravdivá) Hana Rudová, Logické programování I, 5. dubna 2012 2 Rezoluce v PL1 Formule Ji literál l -fc pozitivní literál = atomická formule p(t1, • • • ,tn) &> negativní literál = negace atomické formule —p(t1, • • • ,tn) klauzule C = koneCná množina literálů reprezentující jejich disjunkci príklad: p(X) v q(a,f) v -p(Y) notace: {p (X), q(a, f),-p(Y)} -i- klauzule je pravdivá <=> je pravdivý alespoň jeden z jejích literálů -í* prázdná klauzule se znací □ a je vždy nepravdivá (neexistuje v ní pravdivý literál) -í* formule F = množina klauzulí reprezentující jejich konjunkci A formule je v tzv. konjuktivní normální forme (konjunkce disjunkcí) i> príklad: (p v q) a (-p) a (p v-q v r) notace: {{p, q}, {-p}, {p, -q,r}} A formule je pravdivá <=> všechny klauzule jsou pravdivé J> prázdná formule je vždy pravdivá (neexistuje klauzule, která by byla nepravdivá) M 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í princip ve výrokové logice M Rezoluční princip = pravidlo, které umožňuje odvodit z klauzulí C1 u {l} a {-l} u C2 klauzuli C1 u C2 Ci u {l} C2 Ci u C2 & C1 u C2 se ňazývá rezolventou původních klauzulí Hana Rudová, Logické programování I, 5. dubna 2012 3 Rezoluce v PL1 Rezoluční princip ve výrokové logice Rezoluční princip = pravidlo, které umožňuje odvodit z klauzulí C1 u {l} a {-l} u C2 klauzuli C1 u C2 Ci u {l} C2 Ci u C2 C1 u C2 se ňazývá rezolventou puvodňích klauzulí příklad: {p,r} {—r,s} (p v r) a (-r v s) {p,s} p v s Hana Rudová, Logické programování I, 5. dubna 2012 3 Rezoluce v PL1 Rezoluční princip ve výrokové logiče Rezoluční princip = pravidlo, které umožnuje odvodit z klauzulí Ci u {l} a {-l} u C2 klauzuli Ci u C2 d u {l} {-l}u C2 Ci u C2 C1 u C2 se nazývá rezolventou původních klauzulí príklad: {p,r} {-r, s} (p v r) a (-r v s) {p,s} p v s obe klauzule (p v r) a (-r v s) musí být pravdivé protože r nestačí k pravdivosti obou klauzulí, musí být pravdivé p (pokud je pravdivé -r) nebo s (pokud je pravdivé r), tedy platí klauzule p v s Hana Rudová, Logické programování I, 5. dubna 2012 3 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 Ci je bud' klauzule z F nebo rezolventa Cj, Ck pro k,j < i. Hana Rudová, Logické programování I, 5. dubna 2012 4 Rezoluce v PL1 Rezoluční důkaz rezoluční důkaz klauzule C z formule F je koneCná posloupnost Ci,...,Cn = C klauzulí taková, že Ci je bud' klauzule z F nebo rezolventa Cj, Ck pro k,j < i. & príklad: rezoluCní důkaz {p} z formule F = {{p,r}, {q, —r}, {-q}} Hana Rudová, Logické programování I, 5. dubna 2012 4 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 Ci je bud' klauzule z F nebo rezolventa Cj, Ck pro k,j < i. & príklad: rezoluční důkaz {p} z formule F = {{p,r}, {q, —r}, {-q}} C\ = {p,r} klauzule z F Hana Rudová, Logické programování I, 5. dubna 2012 4 Rezoluce v PL1 Rezoluční důkaz rezoluční důkaz klauzule C z formule F je konecná posloupnost C1,...,Cn = C klauzulí taková, že Ci je bud' klauzule z F nebo rezolventa Cj, Ck pro k,j < i. & príklad: rezolucní důkaz {p} z formule F = {{p,r}, {q, —r}, {-q}} C1 = {p,r} klauzule z F C2 = {q, —r} klauzule z F Hana Rudová, Logické programování I, 5. dubna 2012 4 Rezoluce v PL1 Rezoluční důkaz rezoluční důkaz klauzule C z formule F je konečná posloupnost C\,...,Cn = C klauzulí taková, že Ci je bud' klauzule z F nebo rezolventa Cj, Ck pro k,j < i. & príklad: rezoluční důkaz {p} z formule F = {{p,r}, {q, —r}, {—q}} C\ = {p,r} klauzule z F C2 = {q, —r} klauzule z F C3 = {p, q} rezolventa C\ a C2 Hana Rudová, Logičké programování I, 5. dubna 2012 4 Rezoluče v PL1 Rezoluční důkaz rezoluční důkaz klauzule C z formule F je konecná posloupnost C1,...,Cn = C klauzulí taková, že Ci je bud' klauzule z F nebo rezolventa Cj, Ck pro k,j < i. & príklad: rezolucní důkaz {p} z formule F = {{p,r}, {q, -r}, {-q}} C1 = {p,r} klauzule z F C2 = {q, -r} klauzule z F C3 = {p, q} rezolventa C1 a C2 C4 = {-q} klauzule z F Hana Rudová, Logické programování I, 5. dubna 2012 4 Rezoluce v PL1 Rezoluční důkaz rezoluční důkaz klauzule C z formule F je koneCná posloupnost Ci,...,Cn = C klauzulí taková, že Ci je bud' klauzule z F nebo rezolventa Cj, Ck pro k,j < i. & príklad: rezoluCní dukaz {p} z formule F = {{p,r}, {q, —r}, {-q}} C\ = {p,r} klauzule z F C2 = {q, —r} klauzule z F C3 = {p, q} rezolventa C\ a C2 C4 = {—q} klauzule z F C5 = {p} = C rezolventa C3 a C4 Hana Rudová, Logické programování I, 5. dubna 2012 4 Rezoluce v PL1 Substituce JS> co s promennými? vhodná substituce a unifikace f(X,a,g(Y)) < 1,f(h(c),a,Z) < 1, X = h(c),Z = g(Y) => f(h(c),a,g(Y)) < 1 Hana Rudová, Logické programování I, 5. dubna 2012 5 Rezoluce v PL1 Substituce co s promennými? vhodná substituce a unifikace f(X,a,g(Y)) < 1,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í -i- 9(E) = E pro libovolnou konstantu E 9(f(E1, • • • ,En)) = f (9(E\), • • • , 9(En)) pro libovolný funkcní symbol f -i- 9(p(E1, • • • ,En)) = p(9(E1), • • • , 9(En)) pro libovolný predik. symbol p substituce je tedy homomorfismus výrazů, který zachová vše krome promenných - ty lze nahradit címkoliv substituce zapisujeme zpravidla ve tvaru seznamu [X1/^1, • • • ,Xn/^n] kde Xi jsou promenné a substituované termy príklad: p(X)[X/f(a)] = p(f(a)) Hana Rudová, Logické programování I, 5. dubna 2012 5 Rezoluce v PL1 Substituce JS> co s promennými? vhodná substituce a unifikace f(X,a,g(Y)) < 1,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í -i- 9(E) = E pro libovolnou konstantu E 9(f(E1, • • • ,En)) = f (9(E\), • • • , 9(En)) pro libovolný funkcní symbol f -i* 9(p(E1, • • • ,En)) = p(9(E1), • • • , 9(En)) pro libovolný predik. symbol p JS> substituce je tedy homomorfismus výrazů, který zachová vše krome promenných - ty lze nahradit címkoliv & substituce zapisujeme zpravidla ve tvaru seznamu [X1/^1, • • • ,Xn/^n] kde Xi jsou promenné a "E)i substituované termy príklad: p(X)[X/f(a)] = p(f(a)) & přejmenování promenných: speciální náhrada promenných promennými prí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álu p, q pomocí vhodňé substituce a takové, že pa = qa ňazýváme unifikací a příslušnou substituci unifikátorem. Unifikátorem mňožiňy S literálu nazýváme substituce 0 takovou, že mňožiňa S0 = {t0\t g S} má jediňý prvek. Haňa Rudová, Logické programováňí I, 5. dubňa 2012 6 Rezoluce v PL1 Unifikace Ztotožnení dvou literálu p, q pomocí vhodné substituce a takové, že pa = qa nazýváme unifikací a príslušnou substituci unifikátorem. & Unifikátorem množiny S literál u nazýváme substituce 0 takovou, že množina se = {t0\t g s} má jediný prvek. príklad: S = { datum( D1, M1, 2003 ), datum( 1, M2, Y2) } unifikátor 0 = [D1/1, M1/2, M2/2, Y2/2003] S0 = { datum( 1, 2, 2003 ) } Hana Rudová, Logické programování I, 5. dubna 2012 6 Rezoluce v PL1 Unifikace Ztotožnení dvou literálu p, q pomocí vhodné substituce a takové, že pa = qa nazýváme unifikací a príslušnou substituci unifikátorem. & Unifikátorem množiny S literál u nazýváme substituce 0 takovou, že množina se = {t0\t g s} má jediný prvek. príklad: S = { datum( D1, M1, 2003 ), datum( 1, M2, Y2) } unifikátor 0 = [D1/1, M1/2, M2/2, Y2/2003] S0 = { datum( 1, 2, 2003 ) } & Unifikátor a množiny S nazýváme nejobečnejším unifikátorem (mgu - most generál unifier), jestliže pro libovolný unifikátor 0 existuje substituce A taková, že 0 = aA. Hana Rudová, Logické programování I, 5. dubna 2012 6 Rezoluce v PL1 Unifikace Ztotožnení dvou literálu p, q pomocí vhodné substituce a takové, že pa = qa nazýváme unifikací a príslušnou substituci unifikátorem. & Unifikátorem množiny S literál u nazýváme substituce 0 takovou, že množina se = {t0\t g s} má jediný prvek. príklad: S = { datum( D1, M1, 2003 ), datum( 1, M2, Y2) } unifikátor 0 = [D1/1, M1/2, M2/2, Y2/2003] S0 = { datum( 1, 2, 2003 ) } & Unifikátor a množiny S nazýváme nejobecnejším unifikátorem (mgu - most generál unifier), jestliže pro libovolný unifikátor 0 existuje substituce A taková, že 0 = aA. a príklad (pokrač): nejobecnejší unifikátor a = [D1/1, Y2/2003, M1/M2], Hana Rudová, Logické programování I, 5. dubna 2012 6 Rezoluce v PL1 Unifikace Ztotožnení dvou literálu p, q pomocí vhodné substituce a takové, že pa = qa nazýváme unifikací a príslušnou substituci unifikátorem. & Unifikátorem množiny S literál u nazýváme substituce 0 takovou, že množina se = {t0\t g s} má jediný prvek. príklad: S = { datum( D1, M1, 2003 ), datum( 1, M2, Y2) } unifikátor 0 = [D1/1, M1/2, M2/2, Y2/2003] S0 = { datum( 1, 2, 2003 ) } & Unifikátor a množiny S nazýváme nejobecnejším unifikátorem (mgu - most generál unifier), jestliže pro libovolný unifikátor 0 existuje substituce A taková, že 0 = aA. príklad (pokrač): nejobecnejší unifikátor a = [D1/1, Y2/2003, M1/M2], A=[M2/2] Hana Rudová, Logické programování I, 5. dubna 2012 6 Rezoluce v PL1 Rezoluční prinčip v PL1 základ: & rezolucni princip ve výrokové logice----- Ci u C2 Jť substituce, unifikátor, nejobecnejší unifikátor Hana Rudová, Logické programování I, 5. dubna 2012 7 Rezoluce v PL1 Rezoluční princip v PL1 základ: & rezoluční princip ve výrokové logice----- Ci u C2 Jť substituce, unifikátor, nejobecnejší unifikátor rezoluční princip v PL1 je pravidlo, které -fc pripraví príležitost pro uplatnení vlastního rezolucního pravidla nalezením vhodného unifikátoru provede rezoluci a získá rezolventu Hana Rudová, Logické programování I, 5. dubna 2012 7 Rezoluce v PL1 Rezoluční prinčip v PL1 základ: & rezolucní princip ve výrokové logice----- Ci u C2 Jť substituce, unifikátor, nejobecnejší unifikátor rezoluční prinčip v PL1 je pravidlo, které -fc pripraví príležitost pro uplatnení vlastního rezolucního pravidla nalezením vhodného unifikátoru provede rezoluci a získá rezolventu Ci u {A} {-B}u C2 Cipa u C2a *> kde p je přejmenováním promennýčh takové, že klauzule (Ci u A)p a {B} u C2 nemají spolecné promenné a a je nejobečnejší unifikátor klauzulí Ap a B Hana Rudová, Logické programování I, 5. dubna 2012 7 Rezoluce v PL1 Príklad: rezoluce v PLI C príklad: Ci = {p(X,Y), q(Y)} C2 = {—q(a), s(X,W)} Hana Rudová, Logické programování I, 5. dubna 2012 8 Rezoluce v PL1 Príklad: rezoluce v PLI príklad: Ci = {p(X,Y), q(Y)} C2 = {—q(a), s(X,W)} přejmenování promenných: p = [X/Z] Ci ={p(Z,Y), q(Y)} C2 ={—q(a), s(X,W)} Hana Rudová, Logické programování I, 5. dubna 2012 8 Rezoluce v PL1 Príklad: rezoluče v PLI príklad: Ci = {p(X,Y), q(Y)} C2 = {—q(a), s(X,W)} přejmenování promenných: p = [X/Z] Ci ={p(Z,Y), q(Y)} C2 ={—q(a), s(X,W)} nejobecnejší unifikátor: a = [Y/a] Ci = {p(Z,a), q(a)} C2 = {—q(a), s(X,W)} Hana Rudová, Logické programování I, 5. dubna 2012 8 Rezoluce v PL1 Príklad: rezoluce v PL1 príklad: C1 = {p(X,Y), q(Y)} C2 = {-q(a), s(X,W)} přejmenování promenných: p = [X/Z] C1 = {p(Z,Y), q(Y)} C2 = {-q(a), s(X,W)} nejobecnejší unifikátor: a = [Y/a] C1 = {p(Z,a), q(a)} C2 = {-q(a), s(X,W)} rezolucní princip: C = {p(Z,a), s(X,W)} Hana Rudová, Logické programování I, 5. dubna 2012 8 Rezoluce v PL1 Príklad: rezoluce v PLI príklad: Ci = {p(X,Y), q(Y)} C2 = {-q(a), s(X,W)} přejmenování promenných: p = [X/Z] Ci ={p(Z,Y), q(Y)} C2 = {-q(a), s(X,W)} nejobecnejší unifikátor: a = [Y/a] Ci = {p(Z,a), q(a)} C2 = {-q(a), s(X,W)} rezolucní princip: C = {p(Z,a), s(X,W)} * vyzkoušejte si: Ci = {q(X), -r (Y), p(X,Y), p(f(Z),f(Z))} C2 = {n(Y), -r(W), -p(f(W),f(W)} Hana Rudová, Logické programování I, 5. dubna 2012 8 Rezoluce v PL1 Rezoluce v PLI Obecný rezoluCní princip v PL1 Ci U [Ai, • • • ,Am} {-Bi, • • • , -Bn} u C2 & kde p je přejmenováním proměnných takové, že množiny klauzulí [Aip, • • • ,Amp, Cip} a [Bi, • • • ,Bn, C2} nemají spoleCné promenné Jr a je nejobecnejší unifikátor množiny [Aip, • • • ,Amp,Bi, • • • ,Bn} Hana Rudová, Logické programování I, 5. dubna 2012 9 Rezoluce v PL1 Rezoluce v PL1 Obecný rezolucní princip v PL1 Ci u {Ai, • • • ,Am} {—Bi, , —Bn} u C2 Cipa u C2a & kde p je prejmenováním promenných takové, že množiny klauzulí {A1p, • • • ,Amp, C1p} a {B1, • • • ,Bn, C2} nemají spolecné promenné Jr a je nejobecnejší unifikátor množiny {A1p, • • • ,Amp,B1, • • • ,Bn} príklad: A1 = a(X) vs. {—Bu —B2} = {—a(b), —a(Z)} v jednom kroku potrebuji vyrezolvovat zároven B1 i B2 Hana Rudová, Logické programování I, 5. dubna 2012 9 Rezoluce v PL1 Rezoluce v PL1 Obecný rezolucní princip v PL1 Ci u {Ai, • • • ,Am} {-Bi, • • • , -Bn} u C2 C1 pa u C2a & kde p je přejmenováním proměnných takové, že množiny klauzulí {A1p, • • • ,Amp, C1p} a {B1, • • • ,Bn, C2} nemají spolecné promenné Jr a je nejobecnejší unifikátor množiny {A1p, • • • ,Amp,B1, • • • ,Bn} príklad: A1 = a(X) vs. {-B1, -B2} = {-a(b), -a(Z)} v jednom kroku potrebuji vyrezolvovat zároven B1 i B2 Rezoluce v PL1 a korektní: jestliže existuje rezolucní vyvrácení F, pak F je nesplnitelná & úplná: jestliže F je nesplnitelná, pak existuje rezolucní vyvrácení F Hana Rudová, Logické programování I, 5. dubna 2012 9 Rezoluce v PL1 Zefektivnení rezoluce rezoluce je intuitivne efektivnejší než axiomatické systémy a axiomatické systémy: který z axiomu a pravidel použít? a rezoluce: pouze jedno pravidlo Hana Rudová, Logické programování I, 5. dubna 2012 10 Rezoluce v PL1 Zefektivnení rezoluce rezoluce je intuitivne efektivnejší než axiomatické systémy a axiomatické systémy: který z axiomu a pravidel použít? a rezoluce: pouze jedno pravidlo stále ale príliš mnoho možností, jak hledat dukaz v prohledávacím prostoru problém SAT= {S\S je splnitelná } NP úplný, nicméne: menší prohledávací prostor vede k rychlejšímu nalezení rešení strategie pro zefektivnení prohledávání => varianty rezolucní metody Hana Rudová, Logické programování I, 5. dubna 2012 10 Rezoluce v PL1 Zefektivnení rezoluče $ rezoluce je intuitivne efektivnejší než axiomatické systémy a axiomatické systémy: který z axiomu a pravidel použít? a rezoluce: pouze jedno pravidlo stále ale príliš mnoho možností, jak hledat dukaz v prohledávacím prostoru C- problém SAT= {S\S je splnitelná } NP úplný, nicméne: menší prohledávací prostor vede k rychlejšímu nalezení rešení & strategie pro zefektivnení prohledávání => varianty rezolucní metody & vylepšení prohledávání a zastavit prohledávání cest, které nejsou slibné & specifikace poradí, jak procházíme alternativními cestami Hana Rudová, Logické programování I, 5. dubna 2012 10 Rezoluce v PL1 Varianty rezolucní metody Veta: Každé omezení rezoluce je korektní. & stále víme, že to, co jsme dokázali, platí Hana Rudová, Logické programování I, 5. dubna 2012 11 Rezoluce v PL1 Varianty rezolucní metody Veta: Každé omezení rezoluce je korektní. J* stále víme, že to, co jsme dokázali, platí T-rezoluce: klauzule ucastnící se rezoluce nejsou tautologie úplná -i- tautologie neporrmže ukázat, že formule je nesplnitelná Hana Rudová, Logické programování I, 5. dubna 2012 11 Rezoluce v PL1 Varianty rezolucní metody Veta: Každé omezení rezoluce je korektní. J* stále víme, že to, co jsme dokázali, platí T-rezoluce: klauzule ucastnící se rezoluce nejsou tautologie úplná -i- tautologie neporrmž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ž alespon jednaje v této interpretaci nepravdivá a pokud jsou obe klauzule pravdivé, težko odvodíme nesplnitelnost formule Hana Rudová, Logické programování I, 5. dubna 2012 11 Rezoluce v PL1 Varianty rezoluční metody Veta: Každé omezení rezoluce je korektní. stále víme, že to, co jsme dokázali, platí T-rezoluče: klauzule ucastnící se rezoluce nejsou tautologie úplná -i- tautologie neporrmže ukázat, že formule je nesplnitelná sémantičká rezoluče: úplná zvolíme libovolnou interpretaci a pro rezoluci používáme jen takové klauzule, z nichž alespon jednaje v této interpretaci nepravdivá a pokud jsou obe klauzule pravdivé, težko odvodíme nesplnitelnost formule vstupní (input) rezoluče: neúplná alespon jedna z klauzulí, použitá pri rezoluci, je z výchozí vstupní množiny S Hana Rudová, Logické programování I, 5. dubna 2012 11 Rezoluce v PL1 Varianty rezolucní metody Veta: Každé omezení rezoluce je korektní. & stále víme, že to, co jsme dokázali, platí & T-rezoluce: klauzule ucastnící se rezoluce nejsou tautologie úplná -i- tautologie neporrmže ukázat, že formule je nesplnitelná JS> sémantická rezoluce: úplná zvolíme libovolnou interpretaci a pro rezoluci používáme jen takové klauzule, z nichž alespon jednaje v této interpretaci nepravdivá a pokud jsou obe klauzule pravdivé, težko odvodíme nesplnitelnost formule JS> vstupní (input) rezoluce: neúplná alespon jedna z klauzulí, použitá pri rezoluci, je z výchozí vstupní množiny S {{p, q}, {-p, q}, {p, -q}, {-p, -q}} existuje rezolucní vyvrácení neexistuje rezolucní vyvrácení pomocí vstupní rezoluce Hana Rudová, Logické programování I, 5. dubna 2012 11 Rezoluce v PL1 Rezoluce a logické programování Lineární rezoluce varianta rezolucní metody a snaha o generování lineární posloupnosti místo stromu v každém kroku krome prvního mužeme použít bezprostredne predcházející rezolventu a k tomu bud' nekterou z klauzulí vstupní množiny S nebo nekterou z předcházejících rezolvent C0^B0 C2 B2 c Hana Rudová, Logické programování I, 5. dubna 2012 13 Rezoluce a logické programování Lineární rezoluce varianta rezolucní metody snaha o generování lineární posloupnosti místo stromu v každém kroku krome prvního mužeme použít bezprostredne predcházející rezolventu a k tomu bud' nekterou z klauzulí vstupní množiny S nebo nekterou z predcházejících rezolvent lineární rezolucní důkaz C z S je posloupnost dvojic Ci: strední klauzule & Bi: boční klauzule C Bi {p,q}{p, -1 q} {p} {^p,q} IX □ Hana Rudová, Logické programování I, 5. dubna 2012 14 Rezoluce a logické programování Prologovská notace & Klauzule v matematické logice {H1, ■■■ ,Hm,-T1, ,-Tn} H1 V • • • V Hm V -T1 V • • • V -Tn Hana Rudová, Logické programování I, 5. dubna 2012 15 Rezoluce a logické programování Prologovská notace & Klauzule v matematické logice {H1, ••• ,Hm,-T1, ••• ,-Tn} H1 V • • • V Hm V -T1 V • • • V -Tn & Hornova klauzule: nejvýše jeden pozitivní literál {H,-T1,...,-Tn} {H} {-T1,...,-Tn} a H V -T1 V • • • V -Tn H -T1 V • • • V -Tn Hana Rudová, Logické programování I, 5. dubna 2012 15 Rezoluce a logické programování Prologovská notace & Klauzule v matematické logice {Hi, ■■■ ,Hm,-Ti, --- ,-Tn} Hi V ---V Hm V -Ti V - - - V -Tn & Hornova klauzule: nejvýše jeden pozitivní literál {H,-Ti,...,-Tn} {H} {-Ti,...,-Tn} a H V -Ti V - - - V -Tn H -Ti V - - - V -Tn JS> Pravidlo: jeden pozitivní a alespon jeden negativní literál Prolog: H : - Ti, - - - ,Tn. Hana Rudová, Logické programování I, 5. dubna 2012 15 Rezoluce a logické programování Prologovská notace -i* Klauzule v matematické logice {Hi, ■■■ ,Hm,-Ti, ■■■ ,-Tnj Hi V ■■■V Hm V -Ti V ■ ■ ■ V -Tn ü> Hornova klauzule: nejvýše jeden pozitivní literál {H,-Ti,...,-Tnj {H j {-Ti,...,-Tnj a H V -Ti V ■ ■ ■V -Tn H -Ti V ■ ■ ■V -Tn JS> Pravidlo: jeden pozitivní a alespon jeden negativní literál & Prolog: H : - Ti, ■ ■ ■ ,Tn. Matematická logika: H <= Ti a ■ ■ ■ a Tn Hana Rudová, Logické programování I, 5. dubna 2012 15 Rezoluce a logické programování Prologovská notace & Klauzule v matematické logice [Hu --- ,Hm,-Ti, --- ,-Tn} Hi v ---v Hm v -Ti v - - - v -Tn & Hornova klauzule: nejvýše jeden pozitivní literal [H,-Ti,...,-Tn} [H} [-Ti,...,-Tn} a H v -T1 v - - - v -Tn H -T1 v - - - v -Tn JS> Pravidlo: jeden pozitivní a alespon jeden negativní literal & Prolog: H : - T1, - - - ,Tn. Matematická logika: H <= T1 a - - - a Tn H <= T Hana Rudová, Logické programování I, 5. dubna 2012 15 Rezoluce a logické programování Prologovská notace -i* Klauzule v matematické logice {Hl, ■■■ ,Hm,-Tl, ■■■ ,-Tn} Hl v ■■■v Hm v -Tl v ■ ■ ■ v -Tn ü> Hornova klauzule: ňejvýše jedeň pozitivňí literál {H,-Ti,...,-Tn} {H} {-Ti,...,-Tn} a H v -T1 v ■ ■ ■v -Tn H -T1 v ■ ■ ■v -Tn JS> Pravidlo: jedeň pozitivňí a alespoň jedeň ňegativňí literál & Prolog: H : - T1, ■ ■ ■ ,Tn. Matematická logika: H <= T1 a ■ ■ ■ a Tn Haňa Rudová, Logické programováňí I, S. dubňa 2G12 1S Rezoluce a logické programováňí Prologovská notace & Klauzule v matematické logice {H1, ••• ,Hm,-T1, ••• ,-Tn} H1 v • • • v Hm v -T1 v • • • v -Tn & Hornova klauzule: nejvýše jeden pozitivní literál a H v -T1 v • • • v -Tn H -T1 v • • • v -Tn JS> Pravidlo: jeden pozitivní a alespon jeden negativní literál J* Prolog: H : - T1, • • • ,Tn. Matematická logika: H <= T1 a • • • a Tn M» H <= T H v-T H v-T1 v • • • v -Tn Hana Rudová, Logické programování I, 5. dubna 2012 15 Rezoluce a logické programování Prologovská notace & Klauzule v matematické logice {Hi, --- ,Hm,-Ti, --- ,-Tn} Hi v ---v Hm v -Ti v - - - v -Tn & Hornova klauzule: nejvýše jeden pozitivní literal {H,-Ti,...,-Tn} {H} {-Ti,...,-Tn} a H v -Ti v - - - v -Tn H -Ti v - - - v -Tn JS> Pravidlo: jeden pozitivní a alespon jeden negativní literal & Prolog: H : - Ti, - - - ,Tn. Matematická logika: H <= Ti a - - - a Tn J* H <= T H v-T H v-Ti v---v-Tn Klauzule: {H,-Ti,..., -Tn} Hana Rudová, Logické programování I, 5. dubna 2012 15 Rezoluce a logické programování Prologovská notače & Klauzule v matematické logice {Hi, --- ,Hm, —Ti, --- , —Tn} Hi v ---v Hm v —Ti v • • • v —Tn & Hornova klauzule: nejvýše jeden pozitivní literál {H, —Ti,..., —Tn} {H} { — Ti,..., —Tn} a H v —Ti v - - - v —Tn H —Ti v - - - v —Tn JS> Pravidlo: jeden pozitivní a alespon jeden negativní literál J* Prolog: H : - Ti, - - - ,Tn. Matematická logika: H <= Ti a - - - a Tn M» H <= T H v—T H v—Ti v---v—Tn Klauzule: {H, —Ti,..., —Tn} -í* Fakt: pouze jeden pozitivní literál Prolog: H. Matematická logika: H Klauzule: {H} Hana Rudová, Logické programování I, 5. dubna 2012 15 Rezoluce a logické programování Prologovská notace -i* Klauzule v matematické logice {Hi, ■■■ ,Hm,-Ti, ■■■ ,-Tnj Hi V ■■■V Hm V -Ti V ■ ■ ■ V -Tn ü> Hornova klauzule: nejvýše jeden pozitivní literál {H,-Ti,...,-Tnj {H j {-Ti,...,-Tnj a H V -Tl V ■ ■ ■V -Tn H -Tl V ■ ■ ■V -Tn JS> Pravidlo: jeden pozitivní a alespon jeden negativní literál it Prolog: H : - Tl, ■ ■ ■ ,Tn. Matematická logika: H <= Tl a ■ ■ ■ a Tn -l- H <= T H V-T H V-Tl V ■ ■ ■ V -Tn Klauzule: {H,-Tl,...,-Tnj Fakt: pouze jeden pozitivní literál Prolog: H. Matematická logika: H Klauzule: {Hj & Cílová klauzule: žádný pozitivní literál it Prolog: : - Tl,... Tn. Matematická logika: -Tl V ■ ■ ■ V -Tn Klauzule: {-Tl, ■ ■ ■ -Tnj Hana Rudová, Logické programování I, S. dubna ZClZ lS Rezoluce a logické programování Logický program Programová klauzule: práve jeden pozitivní literál (fakt nebo pravidlo) Logický program: konecná množina programových klauzulí Príklad: Sľ logický program jako množina klauzulí: P ={Pi,P2,P3} Pi ={p}, P2 = {p, -q}, P3 = {q} Hana Rudová, Logické programování I, 5. dubna 2012 16 Rezoluce a logické programování Logický program Programová klauzule: práve jeden pozitivní literál (fakt nebo pravidlo) Logický program: konecná množina programových klauzulí Príklad: a logický program jako množina klauzulí: P = {P1,P2,P3} P1 = {p}, P2 = {p, -q}, P3 = {q} & logický program v prologovské notaci: p. p: -q. q. a 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 & Zacneme s cílovou klauzulí: C0 = G ií> Bocní klauzule vybíráme z programových klauzulí P M G ={-q,-p} P ={Pi,P2,P3} : Pi = {p}, P2 = {p, -q}, P3 = {q} : -q, p. p. p : -q, q. Hana Rudová, Logické programování I, 5. dubna 2012 17 Rezoluce a logické programování Lineární rezoluce pro Hornovy klauzule St Zacneme s cílovou klauzulí: C0 = G St Bocní klauzule vybíráme z programových klauzulí P 3 G = {-q,-p} P ={P1,Pz,P3} : P1 = {p}, P2 = {p, -q}, P3 = {q} * : -q,p. p. p: -q, q. (fl (Pi □ Hana Rudová, Logické programování I, 5. dubna 2012 17 Rezoluce a logické programování Lineární rezoluce pro Hornovy klauzule JS* Zacneme s cílovou klauzulí: C0 = G St Bocní klauzule vybíráme z programových klauzulí P MG = {-q,-p} P ={P1,P2,P3} : P1 = {p}, P2 = {p, -q}, P3 = {q} * : -q,p. p. p: -q, q. \/ \/ {^p} {p} ql {q} \/ \/ □ □ Hana Rudová, Logické programování I, 5. dubna 2012 17 Rezoluce a logické programování Lineární rezoluce pro Hornovy klauzule JS* Zacneme s cílovou klauzulí: C0 = G St Bocní klauzule vybíráme z programových klauzulí P MG ={-q,-p} P ={Pi,P2,P3} : Pi = {p}, P2 = {p, -q}, P3 = {q} * : -q,p. p. p: -q, q. □ □ JS> Strední klauzule jsou cílové klauzule Hana Rudová, Logické programování I, 5. dubna 2012 17 Rezoluce a logické programování Lineární vstupní rezoluce Vstupní rezoluce na P u {G} S» (opakování:) alespon jedna z klauzulí použitá pri rezoluci je z výchozí vstupní množiny & zacneme s cílovou klauzulí: C0 = G J* bocní klauzule jsou vždy z P (tj. jsou to programové klauzule) Hana Rudová, Logické programování I, 5. dubna 2012 18 Rezoluce a logické programování Lineární vstupní rezoluce Vstupní rezoluce na P u {G} S» (opakování:) alespoň jedna z klauzulí použitá pri rezoluci je z výchozí vstupní množiny & zacneme s cílovou klauzulí: C0 = G & bocní klauzule jsou vždy z P (tj. jsou to programové klauzule) (Opakování:) Lineární rezolucní dukaz C z P je posloupnost dvojic (Co,Bo), ... (Cn,Bn) taková, že C = Cn+1 a a C0 a každá Bi jsou prvky P nebo nekteré Cj,j < i S» každá Ci+1, i < n je rezolventa Ci a Bi Hana Rudová, Logické programování I, 5. dubna 2012 18 Rezoluce a logické programování Lineární vstupní rezoluče & Vstupní rezoluče na P u {G} S» (opakování:) alespon jedna z klauzulí použitá pri rezoluci je z výchozí vstupní množiny & zacneme s cílovou klauzulí: C0 = G J* bocní klauzule jsou vždy z P (tj. jsou to programové klauzule) JS* (Opakování:) Lineární rezoluční dukaz C z P je posloupnost dvojic (Co,Bo), ... (Cn,Bn) taková, že C = Cn+i a k C0 a každá Bi jsou prvky P nebo nekteré Cj,j < i S* každá Ci+i, i < n je rezolventa Ci a Bi Lineární vstupní (Linear Input) rezoluče (LI-rezoluče) C z P u {G} posloupnost dvojic {Co,B0), ... {Cn,Bn) taková, že C = Cn+i a a C0 = G a každá Bi jsou prvky P lineární rezoluce + vstupní rezoluce a každá Ci+i, i < n je rezolventa Ci a Bi Hana Rudová, Logické programování I, 5. dubna 2012 18 Rezoluce a logické programování Cíle a fakta pri lineární rezoluči JS> Veta: Je-li S nesplnitelná množina Hornových klauzulí, pak S obsahuje alespon jeden číl a jeden fakt. ± pokud nepoužiji cíl, mám pouze fakta (1 pozit.literál) a pravidla (1 pozit.literál a alespon jeden negat. literál), pri rezoluci mi stále zůstává alespon jeden pozit. literál Hana Rudová, Logické programování I, 5. dubna 2012 19 Rezoluce a logické programování Cíle a fakta pri lineární rezoluci JS> Veta: Je-li S nesplnitelná množina Hornových klauzulí, pak S obsahuje alespon jeden cíl a jeden fakt. ± pokud nepoužiji cíl, mám pouze fakta (1 pozit.literál) a pravidla (1 pozit.literál a alespon jeden negat. literál), pri rezoluci mi stále zůstává alespon jeden pozit. literál & pokud nepoužiji fakt, mám pouze cíle (negat.literály) a pravidla (1 pozit.literál a alespon jeden negat. literál), v rezolvente mi stále zůstávají negativní literály Hana Rudová, Logické programování I, 5. dubna 2012 19 Rezoluce a logické programování Cíle a fakta pri lineární rezoluci JS> Veta: Je-li S nesplnitelná množina Hornových klauzulí, pak S obsahuje alespon jeden cíl a jeden fakt. ± pokud nepoužiji cíl, mám pouze fakta (1 pozit.literál) a pravidla (1 pozit.literál a alespon jeden negat. literál), pri rezoluci mi stále zustává alespon jeden pozit. literál -fc pokud nepoužiji fakt, mám pouze cíle (negat.literály) a pravidla (1 pozit.literál a alespon jeden negat. literál), v rezolvente mi stále zůstávají negativní literály veta: Existuje-li rezolucní důkaz prázdné množiny z množiny S Hornových klauzulí, pak tento rezolucní strom má v listech jedinou cílovou klauzuli. pokud zacnu dukaz pravidlem a faktem, pak dostanu zase pravidlo -i- pokud zacnu dukaz dvema pravidly, pak dostanu zase pravidlo A na dvou faktech rezolvovat nelze Hana Rudová, Logické programování I, 5. dubna 2012 19 Rezoluce a logické programování Cíle a fakta při lineární rezoluci & Veta: 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 pozit.literál) a pravidla (1 pozit.literál a alespon jeden negat. literál), pri rezoluci mi stále zustává alespon jeden pozit. literál & pokud nepoužiji fakt, mám pouze cíle (negat.literály) a pravidla (1 pozit.literál a alespon jeden negat. literál), v rezolvente mi stále zustávají negativní literály veta: Existuje-li rezolucní důkaz prázdné množiny z množiny S Hornových klauzulí, pak tento rezolucní strom má v listech jedinou cílovou klauzuli. Jt pokud zacnu důkaz pravidlem a faktem, pak dostanu zase pravidlo -i- pokud zacnu důkaz dvema pravidly, pak dostanu zase pravidlo Jt na dvou faktech rezolvovat nelze = dokud nepoužiji cíl pracuji stále s množinou faktů a pravidel Hana Rudová, Logické programování I, 5. dubna 2012 19 Rezoluce a logické programování Cíle a fakta pri lineární rezoluci JS> Veta: Je-li S nesplnitelná množina Hornových klauzulí, pak S obsahuje alespon jeden cíl a jeden fakt. ± pokud nepoužiji cíl, mám pouze fakta (1 pozit.literál) a pravidla (1 pozit.literál a alespon jeden negat. literál), pri rezoluci mi stále zůstává alespon jeden pozit. literál & pokud nepoužiji fakt, mám pouze cíle (negat.literály) a pravidla (1 pozit.literál a alespon jeden negat. literál), v rezolvente mi stále zustávají negativní literály veta: Existuje-li rezolucní důkaz prázdné množiny z množiny S Hornových klauzulí, pak tento rezolucní strom má v listech jedinou cílovou klauzuli. pokud zacnu dukaz pravidlem a faktem, pak dostanu zase pravidlo -i- pokud zacnu dukaz dvema pravidly, pak dostanu zase pravidlo -fc na dvou faktech rezolvovat nelze = dokud nepoužiji cíl pracuji stále s množinou faktu a pravidel ± pokud použiji v dukazu cílovou klauzulí, fakta mi ubírají negat.literály, pravidla mi je pridávají, v rezolvente mám stále samé negativní literály, tj. nelze rezolvovat s dalším cílem Hana Rudová, Logické programování I, 5. dubna 2012 19 Rezoluce a logické programování Korektnost a úplnost Veta: Množina S Hornových klauzulí je nesplnitelná, práve když existuje rezolucní vyvrácení S pomocí vstupní rezoluce. M Korektnost platí stejne jako pro ostatní omezení rezoluce * Úplnost LI-rezoluce pro Hornovy klauzule: Necht' 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 rezolucní vyvrácení P u {G} pomocí LI-rezoluce. A vstupní rezoluce pro (obecnou) formuli sama o sobe není úplná => LI-rezoluce aplikovaná na (obecnou) formuli nezarucuje, že nalezeneme dukaz, i když formule platí! Hana Rudová, Logické programování I, 5. dubna 2012 20 Rezoluce a logické programování Korektnost a úplnost Veta: Množina S Hornových klauzulí je nesplnitelná, práve když existuje rezolucní vyvrácení S pomocí vstupní rezoluce. M Korektnost platí stejne jako pro ostatní omezení rezoluce * Úplnost LI-rezoluce pro Hornovy klauzule: Necht' 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 rezolucní vyvrácení P u {G} pomocí LI-rezoluce. A vstupní rezoluce pro (obecnou) formuli sama o sobe není úplná => LI-rezoluce aplikovaná na (obecnou) formuli nezarucuje, že nalezeneme dukaz, i když formule platí! & Význam LI-rezoluce pro Hornovy klauzule: i* P = {Pi, . . . ,Pn}, G = {G i ,...,Gm} iľ LI-rezolucí ukážeme nesplnitelnost Pi a • • • a Pn a (-Gi v • • • v -Gm) Hana Rudová, Logické programování I, 5. dubna 2012 20 Rezoluce a logické programování Korektnost a úplnost Veta: Množina S Hornových klauzulí je nesplnitelná, práve když existuje rezolucní vyvrácení S pomocí vstupní rezoluce. M Korektnost platí stejne jako pro ostatní omezení rezoluce * Úplnost LI-rezoluce pro Hornovy klauzule: Necht' 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 rezolucní vyvrácení P u {G} pomocí LI-rezoluce. A vstupní rezoluce pro (obecnou) formuli sama o sobe není úplná => LI-rezoluce aplikovaná na (obecnou) formuli nezarucuje, že nalezeneme dukaz, i když formule platí! & Význam LI-rezoluce pro Hornovy klauzule: i* P = {P1, . . . , Pn}, G = {G'1 ,...,Gm} iľ LI-rezolucí ukážeme nesplnitelnost P1 a • • • a Pn a (-G1 v • • • v -Gm) pokud tedy predpokládáme, že program {P1,.. .,Pn} platí, tak musí být nepravdivá (-G1 v • • • v -Gm), tj. musí platit G1 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 literalů JS> Uspořádaná klauzule (definite clause) = posloupnost liteřálU -fc nelze volne menit poradí literálU £ Rezoluční princip přo uspořádané klauzule: _{-Ao,-An}_[B1 -Bo,-Bm\_ M uspořádaná řezolventa: {-A0,-Ai-\, -B0p,-Bmp,—Ai+\,-An}j &> p je přejmenování promenných takové, že klauzule {A0,.. .,An} a {B,B0,.. .,Bm}p nemají společné promenné & j je nejobecnejší unifikátor pro Ai a Bp Hana Rudová, Logické programování I, 5. dubna 2012 21 Rezoluce a logické programování Uspořádané klauzule (definite clauses) JS> Klauzule = množina literálů JS> Uspořádaná klauzule (definite clause) = posloupnost literálů -fc nelze volne menit poradí literálů £ RezoluCní princip pro uspořádané klauzule: _{-Ao,-An}_[B1 -Bo,-Bm\_ {-Ao,-Ai-i, -Bop,-BmP,-At+i,-An} j M usporádaná rezolventa: {-A0,-Ai-\, -B0p,-Bmp,—Ai+\,-An}j &> p je přejmenování promenných takové, že klauzule {A0,.. .,An} a {B,B0,.. .,Bm}p nemají společné promenné & j je nejobecnejší unifikátor pro Ai a Bp -í* rezoluce je realizována na literálech -Aij a Bpj je dodržováno poradí literálu, tj. {-B0p,-Bmp}j jde do usporádané rezolventy presne na pozici -Aij Hana Rudová, Logické programování I, 5. dubna 2012 21 Rezoluce a logické programování Usporádané klauzule II. C Usporádáné klauzule _{-Ao,-An}_{B -Bo,-Bm\_ {-Ao,-Ai-1, -Bop,-BmP,-Ai+1,-An} Lineární rezoluce se selekCním pravidlem = SLD-rezoluce (Selected Linear resolution for Definite clauses) it rezoluce it Selekcní pravidlo J* Lineární rezoluce it Definite (uspořádané) klauzule Jt vstupní rezoluce M Selekcní pravidlo R je funkce, která každé neprázdné klauzuli C prirazuje nejaký z jejích literálů R(C) e C it pri rezoluci vybírám z klauzule literál urcený selekcním pravidlem Hana Rudová, Logické programování I, 5. dubna 2012 24 Rezoluce a logické programování SLD-rezoluce JS> Lineární rezoluce se selekcním pravidlem = SLD-rezoluce (Selected Linear resolution for Definite clauses) J» rezoluce *> Selekcní pravidlo Jr Lineární rezoluce a Definite (usporádané) klauzule a vstupní rezoluce -i* Selekcní pravidlo R je funkce, která každé neprázdné klauzuli C prirazuje nejaký z jejích literálů R(C) e C -i- pri rezoluci vybírám z klauzule literál urcený selekcním pravidlem & Pokud se R neuvádí, pak se predpokládá výber nejlevejšího literálu nejlevejší literál vybírá i Prolog Hana Rudová, Logické programování I, 5. dubna 2012 24 Rezoluce a logické programování Lineární rezoluce se selekcním pravidlem P = {{p}, {p, -q}, {q}}, G = {-q,-p} {^q,^p} {q} {^q,^p} {p} výber | výber | y/ nejlevejšího {^P} Jp} nejpravejšího Jq} literálu ' / literálu ' ^ □ □ Hana Rudová, Logické programování I, 5. dubna 2012 25 Rezoluce a logické programování Lineární rezoluce se selekcním pravidlem P = {{p}, {p, -q}, {q}}, G = {-q,-p} {^q,^pj {q} {^q,^p} {p} výber | výber | y/ nejlevejšího {^P} Jp} nejpravejšího Jq} literálu ' / literálu ' ^ □ □ SLD-rezolucní vyvrácení P u {G} pomocí selekcního pravidla R je LD-rezolucní vyvrácení (G0,C0),(Gn,Cn) takové, že G = G0,Gn+1 = □ a R(Gi) je literál rezolvovaný v kroku i Hana Rudová, Logické programování I, 5. dubna 2012 25 Rezoluce a logické programování Lineární rezoluce se selekcním pravidlem JS> SLD-rezolucní vyvrácení P u {G} pomocí selekcního pravidla R je LD-rezolucní vyvrácení (G0,C0),(Gn,Cn) takové, že G = G0,Gn+\ = □ a R(Gt) je literál rezolvovaný v kroku i M SLD-rezoluce - korektní, úplná -í* Efektivita SLD-rezoluce je závislá na £• selekcním pravidle R & způsobu výberu príslušné programové klauzule pro tvorbu rezolventy v Prologu se vybírá vždy klauzule, která je v programu první n literálu □ Hana Rudová, Logické programování I, 5. dubna 2012 25 Rezoluce a logické programování Príklad: SLD-strom t: -p,r. t : -s. p : -q, v. p : - u, w q. s. u. (1) (2) (3) (4) (5) (6) (7) : -1. (D/\ (2) :-p,r. (3)/ \(4) :- s. (5) :- v,r. fall :- u,w,r. (7) :- w,r. .(6) □ fall Hana Rudová, Logické programování I, 5. dubna 2012 26 Rezoluce a logické programování Strom výpoctu (SLD-strom) SLD-strom je strom tvorený všemi možnými výpocetními posloupnostmi logického programu P vzhledem k cíli G Hana Rudová, Logické programování I, 5. dubna 2012 27 Rezoluce a logické programování Strom výpoctu (SLD-strom) SLD-strom je strom tvorený všemi možnými výpočetními posloupnostmi logického programu P vzhledem k cíli G korenem stromu je cílová klauzule G v uzlech stromu jsou rezolventy (rodiče uzlu a programové klauzule) & císlo vybrané programové klauzule pro rezoluci je v príkladu uvedeno jako ohodnocení hrany listy jsou dvojího druhu: a oznacené prázdnou klauzulí - jedná se o úspešné uzly (succes nodes) *> oznacené neprázdnou klauzulí - jedná se o neúspešné uzly (failure nodes) Hana Rudová, Logické programování I, 5. dubna 2012 27 Rezoluce a logické programování Strom výpočtu (SLD-strom) SLD-strom je strom tvorený všemi možnými výpočetními posloupnostmi logického programu P vzhledem k cíli G korenem stromu je cílová klauzule G v uzlech stromu jsou rezolventy (rodiče uzlu a programové klauzule) Jt císlo vybrané programové klauzule pro rezoluci je v príkladu uvedeno jako ohodnocení hrany listy jsou dvojího druhu: Jt oznacené prázdnou klauzulí - jedná se o úspešné uzly (succes nodes) *> oznacené neprázdnou klauzulí - jedná se o neúspešné uzly (failure nodes) úplnost SLD-rezoluce zarucuje existenci cesty od korene k úspešnému uzlu pro každý možný výsledek příslušející cíli G Hana Rudová, Logické programování I, 5. dubna 2012 27 Rezoluce a logické programování