Rezoluce v predikátové logice I. řádu Rezoluce JS> rezoluční princip: z F v A, G v -A odvodit F v G & dokazovací metoda používaná a v Prologu -i* ve většině systémů pro automatické dokazování Hana Rudová, Logické programování I, 28. března 2011 2 Rezoluce v PL1 Rezoluce JS> rezoluční princip: z F v A, G v -A odvodit F v G ü> dokazovací metoda používaná a v Prologu & ve většině systémU pro automatické dokazování & procedura pro vyvrácení %> hledáme dukaz pro negaci formule Jr snažíme se dokázat, že negace formule je nesplnitelná => formule je vždy pravdivá Hana Rudová, Logické programování I, 28. března 2011 2 Rezoluce v PL1 Formule literal l J» pozitivní literal = atomická formule p(t\, • • • ,tn) & negativní literal = negace atomické formule -p(ti, • • • ,tn) Hana Rudová, Logické programování I, 28. brezna 2011 3 Rezoluce v PL1 Formule literál l J» pozitivní literál = atomická formule p(t1, • • • ,tn) s* 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)} A klauzule je pravdivá <=> je pravdivý alespoň jeden z jejích literálů -i- prázdná klauzule se znací □ a je vždy nepravdivá (neexistuje v ní pravdivý literál) Hana Rudová, Logické programování I, 28. března 2011 3 Rezoluce v PL1 Formule literál l J» pozitivní literál = atomická formule p(t1, • • • ,tn) s* 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)} A klauzule je pravdivá <=> je pravdivý alespoň jeden z jejích literálů -i- 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 formule je v tzv. konjuktivní normální forme (konjunkce disjunkcí) J* 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, 28. brezna 2011 3 Rezoluce v PL1 Formule literál l J» pozitivní literál = atomická formule p(t1, • • • ,tn) s* 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)} A klauzule je pravdivá <=> je pravdivý alespoň jeden z jejích literálů -i- 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 formule je v tzv. konjuktivní normální forme (konjunkce disjunkcí) J* príklad: (p v q) a (-p) a (p v-q v r) notace: {{p, q}, {-p}, {p, -q,r}} &> 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, 28. brezna 2011 3 Rezoluce v PL1 Formule literál l J» pozitivní literál = atomická formule p(t1, • • • ,tn) s* 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)} A klauzule je pravdivá <=> je pravdivý alespoň jeden z jejích literálů -i- 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 formule je v tzv. konjuktivní normální forme (konjunkce disjunkcí) J* príklad: (p v q) a (-p) a (p v-q v r) notace: {{p, q}, {-p}, {p, -q,r}} &> formule je pravdivá <=> všechny klauzule jsou pravdivé J* 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, 28. brezna 2011 3 Rezoluce v PL1 Splnitelnost [Opakování:] Interpretace I jazyka L je dána univerzem D a zobrazením, které priradí konstante c prvek D, funkCnímu symbolu f/n n-ární operaci v D a predikátovému symbolu p/n n-ární relaci. príklad: F = {{f(a,b) = f (b,a)}, {f(f(a,a),b) = a}} interpretace ?i: D = Z, a := 1,b := -1,f := " + " Hana Rudová, Logické programování I, 28. března 2011 4 Rezoluce v PL1 Splnitelnost [Opakování:] Interpretace I jazyka L je dána univerzem D a zobrazením, které priradí konstante c prvek D, funkCnímu symbolu f/n n-ární operaci v D a predikátovému symbolu p/n n-ární relaci. príklad: F = {{f(a,b) = f (b,a)}, {f(f(a,a),b) = a}} interpretace 11: D = Z, a := 1,b := -1,f := " + " JS> Formule je splnitelná, existuje-li interpretace, pro kterou je pravdivá a formule je konjunkce klauzulí, tj. všechny klauzule musí být v dané interpretaci pravdivé ± príklad (pokrač): F je splnitelná (je pravdivá v I1) Hana Rudová, Logické programování I, 28. března 2011 4 Rezoluce v PL1 Splnitelnost -i* [Opakování:] Interpretace I jazyka L je dána univerzem D a zobrazením, které priradí konstante c prvek D, funkcnímu symbolu f/n n-ární operaci v D a predikátovému symbolu p/n n-ární relaci. príklad: F = {{f(a,b) = f (b,a)}, {f(f(a,a),b) = a}} interpretace 11: D = Z,a := 1,b := -1,f := " + " JS> Formule je splnitelná, existuje-li interpretace, pro kterou je pravdivá a formule je konjunkce klauzulí, tj. všechny klauzule musí být v dané interpretaci pravdivé ± príklad (pokrac.): 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á -i- tj. neexistuje interpretace, ve které by byly všechny klauzule pravdivé j* prí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, 28. brezna 2011 4 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, 28. března 2011 5 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} {-l} u 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 v s Hana Rudová, Logické programování I, 28. března 2011 5 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 puvodníčh 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, 28. brezna 2011 5 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, 28. března 2011 6 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}} Hana Rudová, Logické programování I, 28. brezna 2011 6 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, 28. brezna 2011 6 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, 28. brezna 2011 6 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 C3 = {p, q} rezolventa C1 a C2 Hana Rudová, Logické programování I, 28. brezna 2011 6 Rezoluce v PL1 RezoluCní důkaz rezoluCní 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}} C\ = {p,r} klauzule z F C2 = {q, -r} klauzule z F C3 = {p, q} rezolventa C\ a C2 C4 = {-q} klauzule z F Hana Rudová, Logické programování I, 28. brezna 2011 6 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 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, 28. brezna 2011 6 Rezoluce v PL1 Rezoluční vyvrácení důkaz pravdivosti formule F spočívá v demonstraci nesplnitelnosti — F j* —F nesplnitelná == —F je nepravdivá ve všech interpretacích == F je vždy pravdivá Hana Rudová, Logické programování I, 28. března 2011 7 Rezoluce v PL1 Rezoluční vyvrácení dukaz pravdivosti formule F spocívá v demonstraci nesplnitelnosti -F & -F nesplnitelná = -F je nepravdivá ve všech interpretacích = F je vždy pravdivá ii> zacneme-li z klauzulí reprezentujících -F, musíme postupným uplatňováním rezolucního principu dospet k prázdné klauzuli □ C Príklad: F...-ia v a Hana Rudová, Logické programování I, 28. brezna 2011 7 Rezoluce v PL1 Rezoluční vyvráčení důkaz pravdivosti formule F spocívá v demonstrači nesplnitelnosti -F & -F nesplnitelná = -F je nepravdivá ve všech interpretacích = F je vždy pravdivá ii> zacneme-li z klauzulí reprezentujících -F, musíme postupným uplatňováním rezolucního principu dospet k prázdné klauzuli □ C Príklad: F... -a v a -F.. .a a -a -F... {{a}, {-a}} Hana Rudová, Logické programování I, 28. brezna 2011 7 Rezoluce v PL1 Rezoluční vyvrácení důkaz pravdivosti formule F spocívá v demonstrači nesplnitelnosti —F j* —F nesplnitelná = —F je nepravdivá ve všech interpretacích = F je vždy pravdivá ii> zacneme-li z klauzulí reprezentujících —F, musíme postupným uplatňováním rezolucního principu dospet k prázdné klauzuli □ C Príklad: F... —a v a —F.. .a a —a —F... {{a}, {—a}} C\ = {a},C2 = {—a} rezolventa C1 a C2 je □, tj. F je vždy pravdivá rezolucní důkaz □ z formule G se nazývá rezoluční vyvráčení formule G -i* a tedy G je nepravdivá ve všech interpretacích, tj. G je nesplnitelná Hana Rudová, Logické programování I, 28. brezna 2011 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: j* koren je označen klauzulí C, listy jsou označeny klauzulemi z F a i* každý uzel, který není listem, má bezprostředními potomky označené klauzulemi C\ a C2 je označen rezolventou klauzulí C a C2 M príklad: F = {{p,r}, {q, -r}, {-q}, {-p}} C = □ {p,r} {q, -r} {-q} {-p} / / / strom rezolučního vyvrácení (rezoluční dukaz □ z F) Hana Rudová, Logičké programování I, 28. brezna 2011 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: j* koren je označen klauzulí C, listy jsou označeny klauzulemi z F a i* každý uzel, který není listem, má bezprostředními potomky označené klauzulemi C\ a C2 je označen rezolventou klauzulí C a C2 M príklad: F = {{p,r}, {q, -r}, {-q}, {-p}} C = □ {p,r} {q, -r} {-q} {-p} IM / / / / / strom rezolučního vyvrácení (rezoluční dukaz □ z F) príklad: {{p,r}, {q, -r}, {-q}, {-p, t}, {-s}, {s,-t}} Hana Rudová, Logičké programování I, 28. brezna 2011 8 Rezoluce v PL1 Substituče JS> čo s promennými? vhodná substituče a unifikače 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, 28. brezna 2011 9 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 0 zobrazující výrazy do výrazů tak, že platí -i- 0(E) = E pro libovolnou konstantu E 0(f(E1, • • • ,En)) = f(0(E1), • • • , 0(En)) pro libovolný funkcní symbol f -i* 0(p(E1, • • • ,En)) = p(0(E1), • • • , 0(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 "E)i substituované termy príklad: p(X)[X/f(a)] = p(f(a)) Hana Rudová, Logické programování I, 28. brezna 2011 9 Rezoluce v PL1 Substituce JS> 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 -i* 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ýrazu, který zachová vše kromě proměnných - ty lze nahradit Čímkoliv -i* 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, 28. března 2011 9 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 S0 = {t0\t g S} má jediný prvek. Hana Rudová, Logické programování I, 28. brezna 2011 10 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, 28. brezna 2011 10 Rezoluce v PL1 Unifikace Ztotožnení dvou literál u 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. Hana Rudová, Logické programování I, 28. brezna 2011 10 Rezoluce v PL1 Unifikače C Ztotožnení dvou literálu p, q pomocí vhodné substituce a takové, že pa = qa nazýváme unifikačí a príslušnou substituci unifikátorem. & Unifikátorem množiny S literálu 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. a príklad (pokrac.): nejobecnejší unifikátor a = [D1/1, Y2/2003, M1/M2], Hana Rudová, Logické programování I, 28. brezna 2011 10 Rezoluce v PL1 Unifikace Ztotožnení dvou literál u 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 O takovou, že množina SO = {tO it g S j má jediný prvek. príklad: S = { datum( Dl, Ml, ZOOS ), datum( l, MZ, YZ) j unifikátor O = [Dl/l, Ml/Z, MZ/Z, YZ/ZOOS] SO = { datum( l, Z, ZOOS ) j Unifikátor a množiny S nazýváme nejobecnejším unifikátorem (mgu - most general unifier), jestliže pro libovolný unifikátor O existuje substituce A taková, že O = aA. príklad (pokrač): nejobecnejší unifikátor a = [Dl/l, YZ/ZOOS, Ml/MZ], A=[MZ/Z] Hana Rudová, Logické programování I, ZS. brezna ZOll lO Rezoluce v PLl Rezoluční princip 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, 28. brezna 2011 11 Rezoluce v PL1 Rezoluční princip v PL1 základ: & rezoluční prinčip ve výrokové logiče----- Ci U C2 Jť substituče, unifikátor, nejobečnejší unifikátor rezoluční prinčip v PL1 je pravidlo, které -fc pripraví príležitost pro uplatnení vlastního rezolučního pravidla nalezením vhodného unifikátoru -** provede rezoluči a získá rezolventu Hana Rudová, Logičké programování I, 28. března 2011 11 Rezoluče v PL1 Rezoluční princip v PL1 základ: & rezoluční prinčip ve výrokové logiče----- Ci U C2 Jť substituče, unifikátor, nejobečnejší unifikátor rezoluční prinčip v PL1 je pravidlo, které -fc pripraví príležitost pro uplatnení vlastního rezolučního pravidla nalezením vhodného unifikátoru -** provede rezoluči a získá rezolventu Ci u {A} {-B}u C2 C1 pa u C2a *> kde p je přejmenováním promennýčh takové, že klauzule (C1 u A)p a {B} u C2 nemají společné promenné a a je nejobečnejší unifikátor klauzulí Ap a B Hana Rudová, Logičké programování I, 28. b rezna 2011 11 Rezoluče v PL1 Príklad: rezoluče v PLI C príklad: Ci = {p(X,Y), q(Y)} C2 = {-q(a), s(X,W)} Hana Rudová, Logičké programování I, 28. brezna 2011 12 Rezoluče v PL1 Príklad: rezoluče v PLI príklad: C1 = {p(X,Y), q(Y)} C2 = {—q(a), s(X,W)} prejmenování promenných: p = [X/Z] C1 ={p(Z,Y), q(Y)} C2 ={—q(a), s(X,W)} Hana Rudová, Logické programování I, 28. b rezna 2011 12 Rezoluce v PL1 Príklad: rezoluce v PLI príklad: Ci = {p(X,Y), q(Y)} C2 = {-q(a), s(X,W)} prejmenová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, 28. b rezna 2011 12 Rezoluce v PL1 Príklad: rezoluče v PL1 príklad: Ci = {p(X,Y), q(Y)} C2 = {-q(a), s(X,W)} prejmenová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)} Hana Rudová, Logické programování I, 28. b rezna 2011 12 Rezoluce v PL1 Príklad: rezoluče v PLI príklad: Ci = {p(X,Y), q(Y)} C2 = {-q(a), s(X,W)} prejmenování promennýčh: p = [X/Z] Ci ={p(Z,Y), q(Y)} C2 = {-q(a), s(X,W)} nejobečnejší unifikátor: a = [Y/a] Ci = {p(Z,a), q(a)} C2 = {-q(a), s(X,W)} rezoluční prinčip: 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á, Logičké programování I, 28. b rezna 2011 12 Rezoluče v PL1 Rezoluce v PL1 Obecný rezolucní princip v PL1 C1 u {A1, • • • ,Am} {-B1, • • • , -Bn} u C2 C1 pa u C2a -t 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} Hana Rudová, Logické programování I, 28. b rezna 2011 13 Rezoluce v PL1 Rezoluce v PLI Obecný rezolucní princip v PL1 Ci u {Ai, • • • ,Am} {-Bi, • • • , -Bn} u C2 Cipa u C2a & kde p je prejmenová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} príklad: Ai = a(X) vs. {-Bi, -B2} = {-a(b), -a(Z)} v jednom kroku potrebuji vyrezolvovat zároven Bi i B2 Hana Rudová, Logické programování I, 28. b rezna 2011 13 Rezoluce v PL1 Rezoluce v PLI Obecný rezolucní princip v PL1 Ci u {Ai, • • • ,Am} {-Bi, • • • , -Bn} u C2 C1 pa u C2a & kde p je prejmenováním promenný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} príklad: Ai = a(X) vs. {-Bi, -B2} = {-a(b), -a(Z)} v jednom kroku potrebuji vyrezolvovat zároven Bi 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, 28. b rezna 2011 13 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 Hana Rudová, Logické programování I, 28. b rezna 2011 14 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, 28. b rezna 2011 14 Rezoluce v PL1 Zefektivnení rezoluce C 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, 28. b rezna 2011 14 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, 28. b rezna 2011 15 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á Hana Rudová, Logické programování I, 28. brezna 2011 15 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 Hana Rudová, Logické programování I, 28. brezna 2011 15 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 vstupní (input) rezoluce: neúplná alespon jedna z klauzulí, použitá pri rezoluci, je z výchozí vstupní množiny S Hana Rudová, Logické programování I, 28. brezna 2011 15 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 nepomuže ukázat, že formule je nesplnitelná JS> 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 JS> vstupní (input) rezoluče: 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, 28. brezna 2011 15 Rezoluce v PL1 Rezoluče a logičké programování Lineární rezoluče varianta rezoluční 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 predčházejíčí rezolventu a k tomu bud' nekterou z klauzulí vstupní množiny S nebo nekterou z predčházejíčíčh rezolvent C0^B0 C2 B2 c Hana Rudová, Logičké programování I, 28. března 2011 17 Rezoluče a logičké 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 Pravidlo: jeden pozitivní a alespon jeden negativní literál Prolog: H : - Ti, - - - ,Tn. Hana Rudová, Logičké programování I, 28. brezna 2011 19 Rezoluče a logičké programování Prologovská notače & Klauzule v matematičké logiče {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. Matematičká logika: H <= Ti a - - - a Tn Hana Rudová, Logičké programování I, 28. brezna 2011 19 Rezoluče a logičké 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 -T1 v ■ ■ ■v -Tn H -T1 v ■ ■ ■v -Tn JS> Pravidlo: jeden pozitivní a alespon jeden negativní literál & Prolog: H : - T1, ■ ■ ■ ,Tn. Matematická logika: H <= T1 a ■ ■ ■ a Tn H <= T Hana Rudová, Logické programování I, ZS. brezna ZOll l9 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 H Hv-T Hana Rudová, Logické programování I, 28. brezna 2011 19 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 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, 28. brezna 2011 19 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 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 Klauzule: {H,-T1,..., -Tn} Hana Rudová, Logické programování I, 28. brezna 2011 19 Rezoluce a logické programování Prologovská notače & 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 JS> Pravidlo: jeden pozitivní a alespon jeden negativní literál j* Prolog: H : - T1, - - - ,Tn. Matematická logika: H <= T1 a - - - a Tn -l- H <= T H v—T H v—T1 v---v—Tn Klauzule: {H, —T1,..., —Tn} -í* Fakt: pouze jeden pozitivní literál Prolog: H. Matematická logika: H Klauzule: {H} Hana Rudová, Logické programování I, 28. brezna 2011 19 Rezoluce a logické programování Prologovská notače -i* Klauzule v matematičké logiče {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 -T1 v ■ ■ ■v -Tn H -T1 v ■ ■ ■v -Tn JS> Pravidlo: jeden pozitivní a alespon jeden negativní literál & Prolog: H : - T1, ■ ■ ■ ,Tn. Matematičká logika: H <= T1 a ■ ■ ■ a Tn M» H <= T H v-T H v-T1 v ■ ■ ■ v -Tn Klauzule: {H,-T1,..., -Tn} Fakt: pouze jeden pozitivní literál Prolog: H. Matematičká logika: H Klauzule: {H} & Cílová klauzule: žádný pozitivní literál it Prolog: : - T1,... Tn. Matematičká logika: -T1 v ■ ■ ■ v -Tn Klauzule: {-T1, ■ ■ ■ -Tn} Hana Rudová, Logičké programování I, ZS. brezna ZOll l9 Rezoluče a logičké 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 ={P1,P2,P3} P1 ={p}, P2 = {p, -q}, P3 = {q} Hana Rudová, Logické programování I, 28. brezna 2011 20 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, 28. brezna 2011 20 Rezoluce a logické programování Lineární rezoluče 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, 28. brezna 2011 21 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 ={Pi,P2,P3} : Pi = {p}, P2 = {p, -q}, P3 = {q} * : -q,p. p. p: -q, q. (fl (Pi □ Hana Rudová, Logické programování I, 28. brezna 2011 21 Rezoluce a logické programování Lineární rezoluce pro Hornovy klauzule JS* Začneme s cílovou klauzulí: C0 = G St Boční 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. {-q,->pl iq) (^q,^pj {q} i^pl {p -1 q} \/ \/ {^p} {p} ql {ql \/ \/ □ □ Hana Rudová, Logičké programování I, 28. brezna 2011 21 Rezoluce a logičké programování Lineární rezoluče 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. □ □ JS> Strední klauzule jsou čílové klauzule Hana Rudová, Logické programování I, 28. brezna 2011 21 Rezoluce a logické programování Lineární vstupní rezoluče Vstupní rezoluče 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) Hana Rudová, Logické programování I, 28. brezna 2011 22 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í: Co = G J* bocní klauzule jsou vždy z P (tj. jsou to programové klauzule) (Opakování:) Lineární rezolucní dukaz C z S je posloupnost dvojic (Co,Bo), ... (Cn,Bn) taková, že C = Cn+1 a k C0 a každá Bi jsou prvky S nebo nekteré Cj,j < i S» každá Ci+1, i < n je rezolventa Ci a Bi Hana Rudová, Logické programování I, 28. brezna 2011 22 Rezoluce a logické programování Lineární vstupní rezoluče & Vstupní rezoluče 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) JS* (Opakování:) Lineární rezoluční dukaz C z S je posloupnost dvojic (Co,Bo), ... (Cn,Bn) taková, že C = Cn+i a k C0 a každá Bi jsou prvky S 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, 28. brezna 2011 22 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 Hana Rudová, Logické programování I, 28. b rezna 2011 23 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 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 Hana Rudová, Logické programování I, 28. března 2011 23 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 -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 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 důkaz pravidlem a faktem, pak dostanu zase pravidlo -i- pokud zacnu důkaz dvema pravidly, pak dostanu zase pravidlo A na dvou faktech rezolvovat nelze Hana Rudová, Logické programování I, 28. brezna 2011 23 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. 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 Hana Rudová, Logické programování I, 28. brezna 2011 23 Rezoluce a logické programování Cíle a fakta pri lineární rezoluči JS> Veta: Je-li S nesplnitelná množina Hornovýčh klauzulí, pak S obsahuje alespon jeden číl a jeden fakt. ± pokud nepoužiji číl, mám pouze fakta (1 pozit.literál) a pravidla (1 pozit.literál a alespon jeden negat. literál), pri rezoluči mi stále zustává alespon jeden pozit. literál -fc pokud nepoužiji fakt, mám pouze čí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 rezoluční důkaz prázdné množiny z množiny S Hornovýčh klauzulí, pak tento rezoluční strom má v listečh jedinou čílovou klauzuli. pokud začnu dukaz pravidlem a faktem, pak dostanu zase pravidlo -i- pokud začnu dukaz dvema pravidly, pak dostanu zase pravidlo A na dvou faktečh rezolvovat nelze => dokud nepoužiji číl pračuji stále s množinou faktu a pravidel ± pokud použiji v dukazu čí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 čílem Hana Rudová, Logičké programování I, 28. brezna 2011 23 Rezoluče a logičké 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, 28. brezna 2011 24 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) Hana Rudová, Logické programování I, 28. brezna 2011 24 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í rezoluče. M Korektnost platí stejne jako pro ostatní omezení rezoluce * Úplnost Ll-rezoluče 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 Ll-rezoluče pro Hornovy klauzule: i* P = {P1, . . . , Pn}, G = {G1 ,...,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, 28. brezna 2011 24 Rezoluce a logické programování