Rezoluce v predikátové logice I. řádu Rezoluce rezoluční princip: z F A, G A odvodit F G dokazovací metoda používaná v Prologu ve většině systémů pro automatické dokazování Hana Rudová, Logické programování I, 30. března 2007 2 Rezoluce v PL1 Rezoluce rezoluční princip: z F A, G A odvodit F 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á Hana Rudová, Logické programování I, 30. března 2007 2 Rezoluce v PL1 Formule literál l pozitivní literál = atomická formule p(t1, , tn) negativní literál = negace atomické formule p(t1, , tn) Hana Rudová, Logické programování I, 30. března 2007 3 Rezoluce v PL1 Formule literál l pozitivní literál = atomická formule p(t1, , tn) negativní literál = negace atomické formule p(t1, , tn) klauzule C = konečná množina literálů reprezentující jejich disjunkci příklad: p(X) q(a, f) p(Y) notace: {p(X), q(a, f), p(Y)} klauzule 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) Hana Rudová, Logické programování I, 30. března 2007 3 Rezoluce v PL1 Formule literál l pozitivní literál = atomická formule p(t1, , tn) negativní literál = negace atomické formule p(t1, , tn) klauzule C = konečná množina literálů reprezentující jejich disjunkci příklad: p(X) q(a, f) p(Y) notace: {p(X), q(a, f), p(Y)} klauzule 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: (p q) (p) (p q r) notace: {{p, q}, {p}, {p, q, r}} Hana Rudová, Logické programování I, 30. března 2007 3 Rezoluce v PL1 Formule literál l pozitivní literál = atomická formule p(t1, , tn) negativní literál = negace atomické formule p(t1, , tn) klauzule C = konečná množina literálů reprezentující jejich disjunkci příklad: p(X) q(a, f) p(Y) notace: {p(X), q(a, f), p(Y)} klauzule 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: (p q) (p) (p q 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á) Hana Rudová, Logické programování I, 30. března 2007 3 Rezoluce v PL1 Formule literál l pozitivní literál = atomická formule p(t1, , tn) negativní literál = negace atomické formule p(t1, , tn) klauzule C = konečná množina literálů reprezentující jejich disjunkci příklad: p(X) q(a, f) p(Y) notace: {p(X), q(a, f), p(Y)} klauzule 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: (p q) (p) (p q 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, 30. března 2007 3 Rezoluce v PL1 Splnitelnost [ Opakování: ] Interpretace I jazyka L je dána univerzem D a zobrazením, které přiřadí konstantě c prvek D, funkčnímu symbolu f/n n-ární operaci v D a predikátovému symbolu p/n n-ární relaci. příklad: F = {{f(a, b) = f (b, a)}, {f(f(a, a), b) = a}} interpretace I1: D = Z, a := 1, b := -1, f := " + " Hana Rudová, Logické programování I, 30. března 2007 4 Rezoluce v PL1 Splnitelnost [ Opakování: ] Interpretace I jazyka L je dána univerzem D a zobrazením, které přiřadí konstantě c prvek D, funkčnímu symbolu f/n n-ární operaci v D a predikátovému symbolu p/n n-ární relaci. příklad: F = {{f(a, b) = f (b, a)}, {f(f(a, a), b) = a}} interpretace I1: D = Z, a := 1, b := -1, f := " + " 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 I1) Hana Rudová, Logické programování I, 30. března 2007 4 Rezoluce v PL1 Splnitelnost [ Opakování: ] Interpretace I jazyka L je dána univerzem D a zobrazením, které přiřadí konstantě c prvek D, funkčnímu symbolu f/n n-ární operaci v D a predikátovému symbolu p/n n-ární relaci. příklad: F = {{f(a, b) = f (b, a)}, {f(f(a, a), b) = a}} interpretace I1: D = Z, a := 1, b := -1, f := " + " 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 I1) 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(a)}} je nesplnitelná ({p(a)} a {p(a)} nemohou být zároveň pravdivé) Hana Rudová, Logické programování I, 30. března 2007 4 Rezoluce v PL1 Rezoluční princip ve výrokové logice Rezoluční princip = pravidlo, které umožňuje odvodit z klauzulí C1 {l} a {l} C2 klauzuli C1 C2 C1 {l} {l} C2 C1 C2 C1 C2 se nazývá rezolventou původních klauzulí Hana Rudová, Logické programování I, 30. března 2007 5 Rezoluce v PL1 Rezoluční princip ve výrokové logice Rezoluční princip = pravidlo, které umožňuje odvodit z klauzulí C1 {l} a {l} C2 klauzuli C1 C2 C1 {l} {l} C2 C1 C2 C1 C2 se nazývá rezolventou původních klauzulí příklad: {p, r} {r, s} {p, s} (p r) (r s) p s Hana Rudová, Logické programování I, 30. března 2007 5 Rezoluce v PL1 Rezoluční princip ve výrokové logice Rezoluční princip = pravidlo, které umožňuje odvodit z klauzulí C1 {l} a {l} C2 klauzuli C1 C2 C1 {l} {l} C2 C1 C2 C1 C2 se nazývá rezolventou původních klauzulí příklad: {p, r} {r, s} {p, s} (p r) (r s) p s obě klauzule (p r) a (r 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 s Hana Rudová, Logické programování I, 30. března 2007 5 Rezoluce v PL1 Rezoluční důkaz rezoluční důkaz klauzule C z formule F je konečná posloupnost C1, . . . , 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, 30. března 2007 6 Rezoluce v PL1 Rezoluční důkaz rezoluční důkaz klauzule C z formule F je konečná posloupnost C1, . . . , Cn = C klauzulí taková, že Ci je bud' klauzule z F nebo rezolventa Cj, Ck pro k, j < i. příklad: rezoluční důkaz {p} z formule F = {{p, r}, {q, r}, {q}} Hana Rudová, Logické programování I, 30. března 2007 6 Rezoluce v PL1 Rezoluční důkaz rezoluční důkaz klauzule C z formule F je konečná posloupnost C1, . . . , Cn = C klauzulí taková, že Ci je bud' klauzule z F nebo rezolventa Cj, Ck pro k, j < i. příklad: rezoluční důkaz {p} z formule F = {{p, r}, {q, r}, {q}} C1 = {p, r} klauzule z F Hana Rudová, Logické programování I, 30. března 2007 6 Rezoluce v PL1 Rezoluční důkaz rezoluční důkaz klauzule C z formule F je konečná posloupnost C1, . . . , Cn = C klauzulí taková, že Ci je bud' klauzule z F nebo rezolventa Cj, Ck pro k, j < i. příklad: rezoluční 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, 30. března 2007 6 Rezoluce v PL1 Rezoluční důkaz rezoluční důkaz klauzule C z formule F je konečná posloupnost C1, . . . , Cn = C klauzulí taková, že Ci je bud' klauzule z F nebo rezolventa Cj, Ck pro k, j < i. příklad: rezoluční 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 Hana Rudová, Logické programování I, 30. března 2007 6 Rezoluce v PL1 Rezoluční důkaz rezoluční důkaz klauzule C z formule F je konečná posloupnost C1, . . . , Cn = C klauzulí taková, že Ci je bud' klauzule z F nebo rezolventa Cj, Ck pro k, j < i. příklad: rezoluční 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, 30. března 2007 6 Rezoluce v PL1 Rezoluční důkaz rezoluční důkaz klauzule C z formule F je konečná posloupnost C1, . . . , Cn = C klauzulí taková, že Ci je bud' klauzule z F nebo rezolventa Cj, Ck pro k, j < i. příklad: rezoluční 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 C5 = {p} = C rezolventa C3 a C4 Hana Rudová, Logické programování I, 30. března 2007 6 Rezoluce v PL1 Rezoluční vyvrácení rezoluční důkaz formule F spočívá v demonstraci nesplnitelnosti F F nesplnitelná F je nepravdivá ve všech interpretacích F je vždy pravdivá Hana Rudová, Logické programování I, 30. března 2007 7 Rezoluce v PL1 Rezoluční vyvrácení rezoluční důkaz formule F spočívá v demonstraci nesplnitelnosti F F nesplnitelná F je nepravdivá ve všech interpretacích F je vždy pravdivá začneme-li z klauzulí reprezentujících F, musíme postupným uplatňováním rezolučního principu dospět k prázdné klauzuli Příklad: F . . . a a Hana Rudová, Logické programování I, 30. března 2007 7 Rezoluce v PL1 Rezoluční vyvrácení rezoluční důkaz formule F spočívá v demonstraci nesplnitelnosti F F nesplnitelná F je nepravdivá ve všech interpretacích F je vždy pravdivá začneme-li z klauzulí reprezentujících F, musíme postupným uplatňováním rezolučního principu dospět k prázdné klauzuli Příklad: F . . . a a F . . . a a F . . . {{a}, {a}} Hana Rudová, Logické programování I, 30. března 2007 7 Rezoluce v PL1 Rezoluční vyvrácení rezoluční důkaz formule F spočívá v demonstraci nesplnitelnosti F F nesplnitelná F je nepravdivá ve všech interpretacích F je vždy pravdivá začneme-li z klauzulí reprezentujících F, musíme postupným uplatňováním rezolučního principu dospět k prázdné klauzuli Příklad: F . . . a a F . . . a a F . . . {{a}, {a}} C1 = {a}, C2 = {a} rezolventa C1 a C2 je , tj. F je vždy pravdivá rezoluční důkaz z formule F se nazývá rezoluční vyvrácení formule F Hana Rudová, Logické programování I, 30. března 2007 7 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 C1 a C2 je označen rezolventou klauzulí C1 a C2 příklad: F = {{p, r}, {q, r}, {q}, {p}} C = {p, r} {q, r} {q} {p} {p, q} {p} d d d d 7 7 7 7 7 7 7 7 7 7 t t t t t( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( strom rezolučního vyvrácení (rezoluční důkaz z F) Hana Rudová, Logické programování I, 30. března 2007 8 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 C1 a C2 je označen rezolventou klauzulí C1 a C2 příklad: F = {{p, r}, {q, r}, {q}, {p}} C = {p, r} {q, r} {q} {p} {p, q} {p} d d d d 7 7 7 7 7 7 7 7 7 7 t t t t t( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( strom rezolučního vyvrácení (rezoluční důkaz z F) příklad: {{p, r}, {q, r}, {q}, {p, t}, {s}, {s, t}} Hana Rudová, Logické programování I, 30. března 2007 8 Rezoluce v PL1 Substituce co s proměnný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, 30. března 2007 9 Rezoluce v PL1 Substituce co s proměnný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 zobrazující výrazy do výrazů tak, že platí (E) = E pro libovolnou konstantu E (f (E1, , En)) = f((E1), , (En)) pro libovolný funkční symbol f (p(E1, , En)) = p((E1), , (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 [X1/1, , Xn/n] kde Xi jsou proměnné a i substituované termy příklad: p(X)[X/f(a)] p(f (a)) Hana Rudová, Logické programování I, 30. března 2007 9 Rezoluce v PL1 Substituce co s proměnný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 zobrazující výrazy do výrazů tak, že platí (E) = E pro libovolnou konstantu E (f (E1, , En)) = f((E1), , (En)) pro libovolný funkční symbol f (p(E1, , En)) = p((E1), , (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 [X1/1, , Xn/n] kde Xi jsou proměnné a i 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, 30. března 2007 9 Rezoluce v PL1 Unifikace Ztotožnění dvou literálů p, q pomocí vhodné substituce takové, že p = q nazýváme unifikací a příslušnou substituci unifikátorem. Unifikátorem množiny S literálů nazýváme substituce takovou, že množina S = {t|t S} má jediný prvek. Hana Rudová, Logické programování I, 30. března 2007 10 Rezoluce v PL1 Unifikace Ztotožnění dvou literálů p, q pomocí vhodné substituce takové, že p = q nazýváme unifikací a příslušnou substituci unifikátorem. Unifikátorem množiny S literálů nazýváme substituce takovou, že množina S = {t|t S} má jediný prvek. příklad: S = { datum( D1, M1, 2003 ), datum( 1, M2, Y2) } unifikátor = [D1/1, M1/2, M2/2, Y2/2003] S = { datum( 1, 2, 2003 ) } Hana Rudová, Logické programování I, 30. března 2007 10 Rezoluce v PL1 Unifikace Ztotožnění dvou literálů p, q pomocí vhodné substituce takové, že p = q nazýváme unifikací a příslušnou substituci unifikátorem. Unifikátorem množiny S literálů nazýváme substituce takovou, že množina S = {t|t S} má jediný prvek. příklad: S = { datum( D1, M1, 2003 ), datum( 1, M2, Y2) } unifikátor = [D1/1, M1/2, M2/2, Y2/2003] S = { datum( 1, 2, 2003 ) } Unifikátor množiny S nazýváme nejobecnějším unifikátorem (mgu ­ most general unifier), jestliže pro libovolný unifikátor existuje substituce taková, že = . Hana Rudová, Logické programování I, 30. března 2007 10 Rezoluce v PL1 Unifikace Ztotožnění dvou literálů p, q pomocí vhodné substituce takové, že p = q nazýváme unifikací a příslušnou substituci unifikátorem. Unifikátorem množiny S literálů nazýváme substituce takovou, že množina S = {t|t S} má jediný prvek. příklad: S = { datum( D1, M1, 2003 ), datum( 1, M2, Y2) } unifikátor = [D1/1, M1/2, M2/2, Y2/2003] S = { datum( 1, 2, 2003 ) } Unifikátor množiny S nazýváme nejobecnějším unifikátorem (mgu ­ most general unifier), jestliže pro libovolný unifikátor existuje substituce taková, že = . příklad (pokrač.): nejobecnější unifikátor = [D1/1, Y2/2003, M1/M2], Hana Rudová, Logické programování I, 30. března 2007 10 Rezoluce v PL1 Unifikace Ztotožnění dvou literálů p, q pomocí vhodné substituce takové, že p = q nazýváme unifikací a příslušnou substituci unifikátorem. Unifikátorem množiny S literálů nazýváme substituce takovou, že množina S = {t|t S} má jediný prvek. příklad: S = { datum( D1, M1, 2003 ), datum( 1, M2, Y2) } unifikátor = [D1/1, M1/2, M2/2, Y2/2003] S = { datum( 1, 2, 2003 ) } Unifikátor množiny S nazýváme nejobecnějším unifikátorem (mgu ­ most general unifier), jestliže pro libovolný unifikátor existuje substituce taková, že = . příklad (pokrač.): nejobecnější unifikátor = [D1/1, Y2/2003, M1/M2], =[M2/2] Hana Rudová, Logické programování I, 30. března 2007 10 Rezoluce v PL1 Rezoluční princip v PL1 základ: rezoluční princip ve výrokové logice C1 {l} {l} C2 C1 C2 substituce, unifikátor, nejobecnější unifikátor Hana Rudová, Logické programování I, 30. března 2007 11 Rezoluce v PL1 Rezoluční princip v PL1 základ: rezoluční princip ve výrokové logice C1 {l} {l} C2 C1 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 Hana Rudová, Logické programování I, 30. března 2007 11 Rezoluce v PL1 Rezoluční princip v PL1 základ: rezoluční princip ve výrokové logice C1 {l} {l} C2 C1 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 C1 {A} {B} C2 C1 C2 kde je přejmenováním proměnných takové, že klauzule (C1 A) a {B} C2 nemají společné proměnné je nejobecnější unifikátor klauzulí A a B Hana Rudová, Logické programování I, 30. března 2007 11 Rezoluce v PL1 Příklad: rezoluce v PL1 příklad: C1 = {p(X, Y), q(Y)} C2 = {q(a), s(X, W)} Hana Rudová, Logické programování I, 30. března 2007 12 Rezoluce v PL1 Příklad: rezoluce v PL1 příklad: C1 = {p(X, Y), q(Y)} C2 = {q(a), s(X, W)} přejmenování proměnných: = [X/Z] C1 = {p(Z, Y), q(Y)} C2 = {q(a), s(X, W)} Hana Rudová, Logické programování I, 30. března 2007 12 Rezoluce v PL1 Příklad: rezoluce v PL1 příklad: C1 = {p(X, Y), q(Y)} C2 = {q(a), s(X, W)} přejmenování proměnných: = [X/Z] C1 = {p(Z, Y), q(Y)} C2 = {q(a), s(X, W)} nejobecnější unifikátor: = [Y/a] C1 = {p(Z, a), q(a)} C2 = {q(a), s(X, W)} Hana Rudová, Logické programování I, 30. března 2007 12 Rezoluce v PL1 Příklad: rezoluce v PL1 příklad: C1 = {p(X, Y), q(Y)} C2 = {q(a), s(X, W)} přejmenování proměnných: = [X/Z] C1 = {p(Z, Y), q(Y)} C2 = {q(a), s(X, W)} nejobecnější unifikátor: = [Y/a] C1 = {p(Z, a), q(a)} C2 = {q(a), s(X, W)} rezoluční princip: C = {p(Z, a), s(X, W)} Hana Rudová, Logické programování I, 30. března 2007 12 Rezoluce v PL1 Příklad: rezoluce v PL1 příklad: C1 = {p(X, Y), q(Y)} C2 = {q(a), s(X, W)} přejmenování proměnných: = [X/Z] C1 = {p(Z, Y), q(Y)} C2 = {q(a), s(X, W)} nejobecnější unifikátor: = [Y/a] C1 = {p(Z, a), q(a)} C2 = {q(a), s(X, W)} rezoluční princip: C = {p(Z, a), s(X, W)} vyzkoušejte si: C1 = {q(X), r(Y), p(X, Y), p(f(Z), f(Z))} C2 = {n(Y), r(W), p(f(a), f(a)), p(f(W), f(W)} Hana Rudová, Logické programování I, 30. března 2007 12 Rezoluce v PL1 Rezoluce v PL1 Obecný rezoluční princip v PL1 C1 {A1, , Am} {B1, , Bn} C2 C1 C2 kde je přejmenováním proměnných takové, že množiny klauzulí {A1, , Am} a {B1, , Bn} nemají společné proměnné je nejobecnější unifikátor množiny {A1, , Am, B1, , Bn} Hana Rudová, Logické programování I, 30. března 2007 13 Rezoluce v PL1 Rezoluce v PL1 Obecný rezoluční princip v PL1 C1 {A1, , Am} {B1, , Bn} C2 C1 C2 kde je přejmenováním proměnných takové, že množiny klauzulí {A1, , Am} a {B1, , Bn} nemají společné proměnné je nejobecnější unifikátor množiny {A1, , Am, B1, , Bn} příklad: A1 = a(X) vs. {B1, B2} = {a(b), a(Z)} v jednom kroku potřebuji vyrezolvovat zároveň B1 i B2 Hana Rudová, Logické programování I, 30. března 2007 13 Rezoluce v PL1 Rezoluce v PL1 Obecný rezoluční princip v PL1 C1 {A1, , Am} {B1, , Bn} C2 C1 C2 kde je přejmenováním proměnných takové, že množiny klauzulí {A1, , Am} a {B1, , Bn} nemají společné proměnné je nejobecnější unifikátor množiny {A1, , Am, B1, , Bn} příklad: A1 = a(X) vs. {B1, B2} = {a(b), a(Z)} v jednom kroku potřebuji vyrezolvovat zároveň B1 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, 30. března 2007 13 Rezoluce v PL1 Zefektivnění rezoluce rezoluce je intuitivně efektivnější než axiomatické systémy axiomatické systémy: který z axiomů a pravidel použít? rezoluce: pouze jedno pravidlo Hana Rudová, Logické programování I, 30. března 2007 14 Rezoluce v PL1 Zefektivnění rezoluce rezoluce je intuitivně efektivnější než axiomatické systémy axiomatické systémy: který z axiomů a pravidel použít? rezoluce: pouze jedno pravidlo stále ale příliš mnoho možností, jak hledat důkaz v prohledávacím prostoru problém SAT= {S|S je splnitelná } NP úplný, nicméně: menší prohledávací prostor vede k rychlejšímu nalezení řešení strategie pro zefektivnění prohledávání varianty rezoluční metody Hana Rudová, Logické programování I, 30. března 2007 14 Rezoluce v PL1 Zefektivnění rezoluce rezoluce je intuitivně efektivnější než axiomatické systémy axiomatické systémy: který z axiomů a pravidel použít? rezoluce: pouze jedno pravidlo stále ale příliš mnoho možností, jak hledat důkaz v prohledávacím prostoru problém SAT= {S|S je splnitelná } NP úplný, nicméně: menší prohledávací prostor vede k rychlejšímu nalezení řešení strategie pro zefektivnění prohledávání 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, 30. března 2007 14 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í Hana Rudová, Logické programování I, 30. března 2007 15 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 učastnící se rezoluce nejsou tautologie úplná tautologie nepomůže ukázat, že formule je nesplnitelná Hana Rudová, Logické programování I, 30. března 2007 15 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 uč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 Hana Rudová, Logické programování I, 30. března 2007 15 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 uč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 Hana Rudová, Logické programování I, 30. března 2007 15 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 uč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, q}, {p, q}, {p, q}, {p, q}} existuje rezoluční vyvrácení neexistuje rezoluční vyvrácení pomocí vstupní rezoluce Hana Rudová, Logické programování I, 30. března 2007 15 Rezoluce v PL1 Rezoluce a logické programování Lineární rezoluce 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 bud' některou z klauzulí vstupní množiny S nebo některou z předcházejících rezolvent C C 0 1 C2 C C n B Bn 1B B0 2 Hana Rudová, Logické programování I, 30. března 2007 17 Rezoluce a logické programování Lineární rezoluce 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 bud' některou z klauzulí vstupní množiny S nebo některou z předcházejících rezolvent C C 0 1 C2 C C n B Bn 1B B0 2 lineární rezoluční důkaz C z S je posloupnost dvojic C0, B0 , . . . Cn, Bn taková, že C = Cn+1 a C0 a každá Bi jsou prvky S nebo některé Cj, j < i každá Ci+1, i n je rezolventa Ci a Bi Hana Rudová, Logické programování I, 30. března 2007 17 Rezoluce a logické programování Lineární rezoluce 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 bud' některou z klauzulí vstupní množiny S nebo některou z předcházejících rezolvent C C 0 1 C2 C C n B Bn 1B B0 2 lineární rezoluční důkaz C z S je posloupnost dvojic C0, B0 , . . . Cn, Bn taková, že C = Cn+1 a C0 a každá Bi jsou prvky S nebo některé Cj, j < i každá Ci+1, i n je rezolventa Ci a Bi lineární vyvrácení S = lineární rezoluční důkaz z S Hana Rudová, Logické programování I, 30. března 2007 17 Rezoluce a logické programování Lineární rezoluce II. příklad: S = {A1, A2, A3, A4} A1 = {p, q} A2 = {p, q} A3 = {p, q} A4 = {p, q} Hana Rudová, Logické programování I, 30. března 2007 18 Rezoluce a logické programování Lineární rezoluce II. příklad: S = {A1, A2, A3, A4} Ci Bi {q} { p, q} { p,q} {p,q} {p} {p, q} {p}{ p} A1 = {p, q} A2 = {p, q} A3 = {p, q} A4 = {p, q} Hana Rudová, Logické programování I, 30. března 2007 18 Rezoluce a logické programování Lineární rezoluce II. příklad: S = {A1, A2, A3, A4} Ci Bi {q} { p, q} { p,q} {p,q} {p} {p, q} {p}{ p} A1 = {p, q} A2 = {p, q} A3 = {p, q} A4 = {p, q} S: vstupní množina klauzulí Ci: střední klauzule Bi: boční klauzule Hana Rudová, Logické programování I, 30. března 2007 18 Rezoluce a logické programování Prologovská notace Klauzule v matematické logice {H1, , Hm, T1, , Tn} H1 Hm T1 Tn Hana Rudová, Logické programování I, 30. března 2007 19 Rezoluce a logické programování Prologovská notace Klauzule v matematické logice {H1, , Hm, T1, , Tn} H1 Hm T1 Tn Hornova klauzule: nejvýše jeden pozitivní literál {H, T1, . . . , Tn} {H} {T1, . . . , Tn} H T1 Tn H T1 Tn Hana Rudová, Logické programování I, 30. března 2007 19 Rezoluce a logické programování Prologovská notace Klauzule v matematické logice {H1, , Hm, T1, , Tn} H1 Hm T1 Tn Hornova klauzule: nejvýše jeden pozitivní literál {H, T1, . . . , Tn} {H} {T1, . . . , Tn} H T1 Tn H T1 Tn Pravidlo: jeden pozitivní a alespoň jeden negativní literál Prolog: H : - T1, , Tn. Hana Rudová, Logické programování I, 30. března 2007 19 Rezoluce a logické programování Prologovská notace Klauzule v matematické logice {H1, , Hm, T1, , Tn} H1 Hm T1 Tn Hornova klauzule: nejvýše jeden pozitivní literál {H, T1, . . . , Tn} {H} {T1, . . . , Tn} H T1 Tn H T1 Tn Pravidlo: jeden pozitivní a alespoň jeden negativní literál Prolog: H : - T1, , Tn. Matematická logika: H T1 Tn Hana Rudová, Logické programování I, 30. března 2007 19 Rezoluce a logické programování Prologovská notace Klauzule v matematické logice {H1, , Hm, T1, , Tn} H1 Hm T1 Tn Hornova klauzule: nejvýše jeden pozitivní literál {H, T1, . . . , Tn} {H} {T1, . . . , Tn} H T1 Tn H T1 Tn Pravidlo: jeden pozitivní a alespoň jeden negativní literál Prolog: H : - T1, , Tn. Matematická logika: H T1 Tn H T Hana Rudová, Logické programování I, 30. března 2007 19 Rezoluce a logické programování Prologovská notace Klauzule v matematické logice {H1, , Hm, T1, , Tn} H1 Hm T1 Tn Hornova klauzule: nejvýše jeden pozitivní literál {H, T1, . . . , Tn} {H} {T1, . . . , Tn} H T1 Tn H T1 Tn Pravidlo: jeden pozitivní a alespoň jeden negativní literál Prolog: H : - T1, , Tn. Matematická logika: H T1 Tn H T H T Hana Rudová, Logické programování I, 30. března 2007 19 Rezoluce a logické programování Prologovská notace Klauzule v matematické logice {H1, , Hm, T1, , Tn} H1 Hm T1 Tn Hornova klauzule: nejvýše jeden pozitivní literál {H, T1, . . . , Tn} {H} {T1, . . . , Tn} H T1 Tn H T1 Tn Pravidlo: jeden pozitivní a alespoň jeden negativní literál Prolog: H : - T1, , Tn. Matematická logika: H T1 Tn H T H T H T1 Tn Hana Rudová, Logické programování I, 30. března 2007 19 Rezoluce a logické programování Prologovská notace Klauzule v matematické logice {H1, , Hm, T1, , Tn} H1 Hm T1 Tn Hornova klauzule: nejvýše jeden pozitivní literál {H, T1, . . . , Tn} {H} {T1, . . . , Tn} H T1 Tn H T1 Tn Pravidlo: jeden pozitivní a alespoň jeden negativní literál Prolog: H : - T1, , Tn. Matematická logika: H T1 Tn H T H T H T1 Tn Klauzule: {H, T1, . . . , Tn} Hana Rudová, Logické programování I, 30. března 2007 19 Rezoluce a logické programování Prologovská notace Klauzule v matematické logice {H1, , Hm, T1, , Tn} H1 Hm T1 Tn Hornova klauzule: nejvýše jeden pozitivní literál {H, T1, . . . , Tn} {H} {T1, . . . , Tn} H T1 Tn H T1 Tn Pravidlo: jeden pozitivní a alespoň jeden negativní literál Prolog: H : - T1, , Tn. Matematická logika: H T1 Tn H T H T H T1 Tn Klauzule: {H, T1, . . . , Tn} Fakt: pouze jeden pozitivní literál Prolog: H. Matematická logika: H Klauzule: {H} Hana Rudová, Logické programování I, 30. března 2007 19 Rezoluce a logické programování Prologovská notace Klauzule v matematické logice {H1, , Hm, T1, , Tn} H1 Hm T1 Tn Hornova klauzule: nejvýše jeden pozitivní literál {H, T1, . . . , Tn} {H} {T1, . . . , Tn} H T1 Tn H T1 Tn Pravidlo: jeden pozitivní a alespoň jeden negativní literál Prolog: H : - T1, , Tn. Matematická logika: H T1 Tn H T H T H T1 Tn Klauzule: {H, T1, . . . , Tn} Fakt: pouze jeden pozitivní literál Prolog: H. Matematická logika: H Klauzule: {H} Cílová klauzule: žádný pozitivní literál Prolog: : - T1, . . . Tn. Matematická logika: T1 Tn Klauzule: {T1, Tn} Hana Rudová, Logické programování I, 30. března 2007 19 Rezoluce a logické programování