Rezoluce v predikátové logice I. řádu Rezoluce -• rezoluční princip: z i7 v A, G v ->A odvodit F v G -• dokazovací metoda používaná -• v Prologu M ve většině systémů pro automatické dokazování Hana Rudová, Logické programování I, 7. dubna 2009 2 Rezoluce -• rezoluční princip: z F v A, G v ->A odvodit F v G -• dokazovací metoda používaná -• v Prologu M ve většině systémů pro automatické dokazování -• procedura pro vyvrácení 3 hledáme důkaz pro negaci formule M snažíme se dokázat, že negace formule je nesplnitelná => formule je vždy pravdivá Hana Rudová, Logické programování I, 7. dubna 2009 2 Formule M literal I M pozitivní literal = atomická formule p(ti, ■ ■ ■ , tn) M negativní literal = negace atomické formule ^p(t\, ■ ■ ■ , tn) Hana Rudová, Logické programování I, 7. dubna 2009 3 Rezoluce v PL1 Formule M literal I M pozitivní literal = atomická formule p(ti, ■ ■ ■ , tn) M negativní literal = negace atomické formule ^p(t\, ■ ■ ■ ,tn) -• klauzule C = konečná množina literálů reprezentující jejich disjunkci M příklad: p(X) v q(a,f) v ^p(Y) notace: {p(X),q(a,f),^p(Y)} M klauzule je pravdivá <=> je pravdivý alespoň jeden z jejích literálů 3 prázdná klauzule se značí D a je vždy nepravdivá (neexistuje v ní pravdivý literal) Hana Rudová, Logické programování I, 7. dubna 2009 3 Rezoluce v PL1 Formule M literal I M pozitivní literal = atomická formule p(ti, ■ ■ ■ , tn) M negativní literal = negace atomické formule ^p(t\, ■ ■ ■ ,tn) -• klauzule C = konečná množina literálů reprezentující jejich disjunkci M příklad: p(X) v q(a,f) v ^p(Y) notace: {p(X),q(a,f),^p(Y)} M klauzule je pravdivá <=> je pravdivý alespoň jeden z jejích literálů 3 prázdná klauzule se značí D a je vždy nepravdivá (neexistuje v ní pravdivý literal) -• formule F = množina klauzulí reprezentující jejich konjunkci M formule je v tzv. konjuktivní normální formě (konjunkce disjunkcí) M příklad: (p v q) a (^p) a (p v ->g v r) notace: {{p,q}, {^p}, {p, ^q,r}} Hana Rudová, Logické programování I, 7. dubna 2009 3 Rezoluce v PL1 Formule M literal I M pozitivní literal = atomická formule p(ti, ■ ■ ■ , tn) M negativní literal = negace atomické formule ^p(t\, ■ ■ ■ ,tn) -• klauzule C = konečná množina literálů reprezentující jejich disjunkci M příklad: p(X) v q(a,f) v ^p(Y) notace: {p(X),q(a,f),^p(Y)} M klauzule je pravdivá <=> je pravdivý alespoň jeden z jejích literálů 3 prázdná klauzule se značí D a je vždy nepravdivá (neexistuje v ní pravdivý literal) -• formule F = množina klauzulí reprezentující jejich konjunkci M formule je v tzv. konjuktivní normální formě (konjunkce disjunkcí) M příklad: (p v q) a (^p) a (p v ->g v r) notace: {{p,q}, {^p}, {p, ^q,r}} 3 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, 7. dubna 2009 3 Rezoluce v PL1 Formule M literal I M pozitivní literal = atomická formule p(ti, ■ ■ ■ , tn) M negativní literal = negace atomické formule ^p(t\, ■ ■ ■ ,tn) -• klauzule C = konečná množina literálů reprezentující jejich disjunkci M příklad: p(X) v q(a,f) v ^p(Y) notace: {p(X),q(a,f),^p(Y)} M klauzule je pravdivá <=> je pravdivý alespoň jeden z jejích literálů 3 prázdná klauzule se značí D a je vždy nepravdivá (neexistuje v ní pravdivý literal) -• formule F = množina klauzulí reprezentující jejich konjunkci M formule je v tzv. konjuktivní normální formě (konjunkce disjunkcí) M příklad: (p v q) a (^p) a (p v ->g v r) notace: {{p,q}, {^p}, {p, ^q,r}} 3 formule je pravdivá <=> všechny klauzule jsou pravdivé -• prázdná formule je vždy pravdivá (neexistuje klauzule, která by byla nepravdivá) M množinová notace: literal je prvek klauzule, klauzule je prvek formule, ... Hana Rudová, Logické programování I, 7. dubna 2009 3 Rezoluce v PL1 Splnitelnost -• [Opakování:] Interpretace 1 jazyka L je dána univerzem V a zobrazením, které přiřadí konstantě c prvek D, funkčnímu symbolu f/n n-ární operaci v 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 li: D = Z, a := 1, b := -l,f:= " + " Hana Rudová, Logické programování I, 7. dubna 2009 4 Rezoluce v Splnitelnost -• [Opakování:] Interpretace 1 jazyka L je dána univerzem V a zobrazením, které přiřadí konstantě c prvek D, funkčnímu symbolu f/n n-ární operaci v V 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 li: D = Z, a := 1, b := -l,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 li) Hana Rudová, Logické programování I, 7. dubna 2009 4 Rezoluce v PL1 Splnitelnost -• [Opakování:] Interpretace 1 jazyka L je dána univerzem V a zobrazením, které přiřadí konstantě c prvek D, funkčnímu symbolu f/n n-ární operaci v V 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 li. D = Z, a := 1, b := -l,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 li) 3 Formule je nesplnitelná, neexistuje-li interpretace, pro kterou je pravdivá M tj. formule je ve všech iterpretacích nepravdivá 3 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, 7. dubna 2009 4 Rezoluce v PL1 Rezoluční princip ve výrokové logice -• Rezoluční princip = pravidlo, které umožňuje odvodit z klauzulí C\ u {í} a {^1} u C2 klauzuli C\ u C2 QU {ř} {n[}uC2 d uC2 «• Q u C2 se nazývá rezolventou původních klauzulí Hana Rudová, Logické programování I, 7. dubna 2009 5 Rezoluce v PL1 Rezoluční princip ve výrokové logice Rezoluční princip = pravidlo, které umožňuje odvodit z klauzulí C\ u {í} a {^1} u C2 klauzuli C\ u C2 QU {ř} {n[}uC2 d uC2 Q u C2 se nazývá rezolventou původních klauzulí príklad: {p,r] {-■r,5} (p v r) a (->r v s) {p,s] pvs Hana Rudová, Logické programování I, 7. dubna 2009 5 Rezoluce v PLI Rezoluční princip ve výrokové logice Rezoluční princip = pravidlo, které umožňuje odvodit z klauzulí C\ u {í} a {^1} u C2 klauzuli C\ u C2 ClU{ř} {n[}uC2 Ci uC2 Q u C2 se nazývá rezolventou původních klauzulí příklad: {p,r} {^r,s} (p v r) a (->r v s) {p,s} pvs obě klauzule (p v r) a (->r v 5) 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, 7. dubna 2009 5 Rezoluce v PL1 Rezoluční důkaz 3 rezoluční důkaz klauzule C z formule F je konečná posloupnost L-\, ■ ■ ■ j {—ti = C- Kl auzulí taková, že Q je buď klauzule z i7 nebo rezolventa C7, Q pro k,j < í. Hana Rudová, Logické programování I, 7. dubna 2009 6 Rezoluce v PL1 Rezoluční důkaz 3 rezoluční důkaz klauzule C z formule F je konečná posloupnost auzulí taková, že Q je buď klauzule z i7 nebo rezolventa C,, Q pro k,j < í. M příklad: rezoluční důkaz {p} z formule F = {{p,r}, {q, ->r}, {->g}} Hana Rudová, Logické programování I, 7. dubna 2009 6 Rezoluce v PLI Rezoluční důkaz 3 rezoluční důkaz klauzule C z formule F je konečná posloupnost auzulí taková, že Q je buď klauzule z i7 nebo rezolventa C,, Q pro k,j < í. M příklad: rezoluční důkaz {p} z formule F = {{p,r}, {q, ->r}, {->g}} Q = {p,r} klauzule z i7 Hana Rudová, Logické programování I, 7. dubna 2009 6 Rezoluce v PLI Rezoluční důkaz 3 rezoluční důkaz klauzule C z formule F je konečná posloupnost auzulí taková, že Q je buď klauzule z i7 nebo rezolventa C,, Q pro k,j < í. M příklad: rezoluční důkaz {p} z formule F = {{p,r}, {q, ->r}, {->g}} Q = {p,r} klauzule z i7 Q = {^, ~1^} klauzule z i7 Hana Rudová, Logické programování I, 7. dubna 2009 6 Rezoluce v PLI Rezoluční důkaz 3 rezoluční důkaz klauzule C z formule F je konečná posloupnost auzulí taková, že Q je buď klauzule z i7 nebo rezolventa C,, Q pro k,j < í. M příklad: rezoluční důkaz {p} z formule F = {{p,r}, {q, ->r}, {->g}} Q = {p,r} klauzule z i7 Q = {^, ~1^} klauzule z i7 C3 = {p, q} rezolventa C\ a C2 Hana Rudová, Logické programování I, 7. dubna 2009 6 Rezoluce v PLI Rezoluční důkaz 3 rezoluční důkaz klauzule C z formule F je konečná posloupnost auzulí taková, že Q je buď klauzule z i7 nebo rezolventa C,, Q pro k,j < í. M příklad: rezoluční důkaz {p} z formule F = {{p,r}, {q, ->r}, {->g}} Q = {p,r} klauzule z i7 Q = {^, ~1^} klauzule z i7 C3 = {p, q} rezolventa C\ a C2 C4 = {-"^} klauzule z i7 Hana Rudová, Logické programování I, 7. dubna 2009 6 Rezoluce v PLI Rezoluční důkaz 3 rezoluční důkaz klauzule C z formule F je konečná posloupnost auzulí taková, že Q je buď klauzule z i7 nebo rezolventa C,, Q pro k,j < í. M příklad: rezoluční důkaz {p} z formule F = {{p,r}, {q, ->r}, {->g}} Q = {p,r} klauzule z i7 Q = {^, ~1^} klauzule z i7 C3 = {p, q} rezolventa C\ a C2 C4 = {-"^} klauzule z i7 C5 = {p} = C rezolventa C3 a C4 Hana Rudová, Logické programování I, 7. dubna 2009 6 Rezoluce v PLI Rezoluční vyvrácení -• důkaz pravdivosti formule F spočívá v demonstraci nesplnitelnosti ->F M ^F nesplnitelná => ^F je nepravdivá ve všech interpretacích => F je vždy pravdivá Hana Rudová, Logické programování I, 7. dubna 2009 7 Rezoluce v PL1 Rezoluční vyvrácení -• důkaz pravdivosti formule F spočívá v demonstraci nesplnitelnosti ->F M ^F nesplnitelná => ^F je nepravdivá ve všech interpretacích => F je vždy pravdivá M začneme-li z klauzulí reprezentujících -"i7, musíme postupným uplatňováním rezolučního principu dospět k prázdné klauzuli D 3 Příklad: F... -"a v a Hana Rudová, Logické programování I, 7. dubna 2009 7 Rezoluce v PL1 Rezoluční vyvrácení -• důkaz pravdivosti formule F spočívá v demonstraci nesplnitelnosti ->F M ^F nesplnitelná => ^F je nepravdivá ve všech interpretacích => F je vždy pravdivá M začneme-li z klauzulí reprezentujících -"i7, musíme postupným uplatňováním rezolučního principu dospět k prázdné klauzuli D 3 Příklad: F... -"a v a -■i7... a a -"a ^F...{{a},{^a}} Hana Rudová, Logické programování I, 7. dubna 2009 7 Rezoluce v PL1 Rezoluční vyvrácení -• důkaz pravdivosti formule F spočívá v demonstraci nesplnitelnosti ->F M ^F nesplnitelná => ^F je nepravdivá ve všech interpretacích => F je vždy pravdivá M začneme-li z klauzulí reprezentujících -"i7, musíme postupným uplatňováním rezolučního principu dospět k prázdné klauzuli D 3 Příklad: F... -"a v a -■i7... a a -"a ^F...{{a},{^a}} Ci = {a}Xi = í^a] rezolventa C\ a C2 je D, tj. F je vždy pravdivá -• rezoluční důkaz D z formule G se nazývá rezoluční vyvrácení formule G .# a tedy G je nepravdivá ve všech interpretacích, tj. G je nesplnitelná Hana Rudová, Logické programování I, 7. dubna 2009 7 Rezoluce v PL1 Strom rezolučního důkazu -• strom rezolučního důkazu klauzule C z formule i7 je binární strom: M kořen je označen klauzulí C, M listy jsou označeny klauzulemi z F a M každý uzel, který není listem, X má bezprostředními potomky označené klauzulemi C\ a C2 varianty rezoluční metody Hana Rudová, Logické programování I, 7. dubna 2009 14 Rezoluce v PL1 Zefektivnění rezoluce -• rezoluce je intuitivně efektivnější než axiomatické systémy M axiomatické systémy: který z axiomů a pravidel použít? M 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í 3 zastavit prohledávání cest, které nejsou slibné M specifikace pořadí, jak procházíme alternativními cestami Hana Rudová, Logické programování I, 7. dubna 2009 14 Rezoluce v PL1 84 Varianty rezoluční metody -• Věta: Každé omezení rezoluce je korektní. M stále víme, že to, co jsme dokázali, platí Hana Rudová, Logické programování I, 7. dubna 2009 15 Rezoluce v PL1 Varianty rezoluční metody -• Věta: Každé omezení rezoluce je korektní. M stále víme, že to, co jsme dokázali, platí M r-rezoluce: klauzule účastnící se rezoluce nejsou tautologie úplná M tautologie nepomůže ukázat, že formule je nesplnitelná Hana Rudová, Logické programování I, 7. dubna 2009 15 Rezoluce v PL1 Varianty rezoluční metody -• Věta: Každé omezení rezoluce je korektní. M stále víme, že to, co jsme dokázali, platí M r-rezoluce: klauzule účastnící se rezoluce nejsou tautologie úplná M 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ň jednaje v této interpretaci nepravdivá 3 pokud jsou obě klauzule pravdivé, těžko odvodíme nesplnitelnost formule Hana Rudová, Logické programování I, 7. dubna 2009 15 Rezoluce v PL1 Varianty rezoluční metody -• Věta: Každé omezení rezoluce je korektní. M stále víme, že to, co jsme dokázali, platí M r-rezoluce: klauzule účastnící se rezoluce nejsou tautologie úplná M 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ň jednaje v této interpretaci nepravdivá M 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, 7. dubna 2009 15 Rezoluce v PL1 Varianty rezoluční metody -• Věta: Každé omezení rezoluce je korektní. M stále víme, že to, co jsme dokázali, platí M r-rezoluce: klauzule účastnící se rezoluce nejsou tautologie úplná M 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ň jednaje v této interpretaci nepravdivá M 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, 7. dubna 2009 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 buď některou z klauzulí vstupní množiny S nebo některou z předcházejících rezolvent C o B o C, Bj C2 B2 C n B n C Hana Rudová, Logické programování I, 7. dubna 2009 17 Rezoluce a logické programování Lineární rezoluce varianta rezoluční metody M snaha o generování lineární posloupnosti místo stromu -• v každém kroku kromě prvního můžeme použít bezprostředně předcházející rezolventu a k tomu buď některou z klauzulí vstupní množiny S nebo některou z předcházejících rezolvent lineární rezoluční důkaz C z S je posloupnost dvojic (Co,ßo>, ■ ■ ■ (Cn,Bn) taková, že C = Cn+i a 3 Co a každá ßi jsou prvky 5 nebo některé Cj,j < í -• každá Q+i, í < n je rezolventa Q a £í C o C C 2 c B o B B 2 n B n C Hana Rudová, Logické programování I, 7. dubna 2009 17 Rezoluce a logické programování Lineární rezoluce varianta rezoluční metody M snaha o generování lineární posloupnosti místo stromu -• v každém kroku kromě prvního můžeme použít bezprostředně předcházející rezolventu a k tomu buď některou z klauzulí vstupní množiny S nebo některou z předcházejících rezolvent lineární rezoluční důkaz C z S je posloupnost dvojic (Co,ßo>, ■ ■ ■ (Cn,Bn) taková, že C = Cn+i a 3 Co a každá ßi jsou prvky 5 nebo některé Cj,j < í -• každá Q+i, í < n je rezolventa Q a £í lineární vyvrácení 5 = lineární rezoluční důkaz D z S C o C C 2 C n B o B B 2 B n C Hana Rudová, Logické programování I, 7. dubna 2009 17 Rezoluce a logické programování Lineární -• příklad: 5 = {Ai,A2,A3,A4} Ai= {p,q} A2 = {p,^q} A3 = {^P,q} A4 = {^P,^q} Hana Rudová, Logické programování I, 7. dubna 2009 rezoluce I. 18 Rezoluce a logické programování Lineární -• příklad: 5 = {Ai,A2,A3,A4} Ai= {p,q} A2 = {p,^q} A3 = {^P,q} A4 = {^P,^q} Hana Rudová, Logické programování I, 7. dubna 2009 rezoluce I. C t B i {p,q} {p, ^q} \/ {p} {^p>qJ \/ \/ í^p} {p} D 18 Rezoluce a logické programování Lineární -• příklad: 5 = {Ai,A2,A3,A4} Ai= {p,q} A2 = {p,^q} A3 = {^P,q} A4 = {^P,^q} M S\ vstupní množina klauzulí -• Q: střední klauzule -• Bf boční klauzule Hana Rudová, Logické programování I, 7. dubna 2009 rezoluce I. {p,q} {p, ^q} \/ {p} {^p>qJ \/ \/ í^p} {p} D 18 Rezoluce a logické programování Prologovská notace -• Klauzule v matematické logice * {Hi,- ■ ■ ,Hm,-.7i,- ■ ■ ,-.Tn} Hi V ■ ■ ■ vHmV-Ti V ■ ■ ■ v-T, Hana Rudová, Logické programování I, 7. dubna 2009 19 Rezoluce a logické programování Prologovská notace -• Klauzule v matematické logice * {Hi,- ■ ■ ,Hm,-.7i,- ■ ■ ,-.Tn} Hi V ■ ■ ■ vHmV-Ti V ■ ■ ■ v-T, -• Hornova klauzule: nejvýše jeden pozitivní literal * {H,-.Ti,...,-.rn} {H} {-.7i,...,-.rn} -• h v -Ti v ■ ■ ■ v -rn h -Ti v ■ ■ ■ v -rn Hana Rudová, Logické programování I, 7. dubna 2009 19 Rezoluce a logické programování Prologovská notace -• Klauzule v matematické logice * {Hi,- ■ ■ ,Hm,-.7i,- ■ ■ ,-.Tn} Hi V ■ ■ ■ vHmV-Ti V ■ ■ ■ v-T, -• Hornova klauzule: nejvýše jeden pozitivní literal * {H,-.Ti,...,-.rn} {H} {-.7i,...,-.rn} -• h v -Ti v ■ ■ ■ v -rn h -Ti v ■ ■ ■ v -rn -• Pravidlo: jeden pozitivní a alespoň jeden negativní literal M Prolog: H \ - Ti, ■ ■ ■ ,Tn. Hana Rudová, Logické programování I, 7. dubna 2009 19 Rezoluce a logické programování Prologovská notace -• Klauzule v matematické logice * {Hi,- ■ ■ ,Hm,-.7i,- ■ ■ ,-.Tn} Hi V ■ ■ ■ vHmV-Ti V ■ ■ ■ v-T, -• Hornova klauzule: nejvýše jeden pozitivní literal * {H,-.Ti,...,-.rn} {H} {-.7i,...,-.rn} -• h v -Ti v ■ ■ ■ v -rn h -Ti v ■ ■ ■ v -rn -• Pravidlo: jeden pozitivní a alespoň jeden negativní literal -• Prolog: H : - T\, ■ ■ ■ , Tn. Matematická logika: H <= T\ a ■ ■ ■ a T, Hana Rudová, Logické programování I, 7. dubna 2009 19 Rezoluce a logické programování Prologovská notace -• Klauzule v matematické logice * {Hi,- ■ ■ ,Hm,-.7i,- ■ ■ ,-.Tn} Hi V ■ ■ ■ vHmV-Ti V ■ ■ ■ v-T, -• Hornova klauzule: nejvýše jeden pozitivní literal * {H,-.Ti,...,-.rn} {H} {-.7i,...,-.rn} -• h v -Ti v ■ ■ ■ v -rn h -Ti v ■ ■ ■ v -rn -• Pravidlo: jeden pozitivní a alespoň jeden negativní literal -• Prolog: H : - T\, ■ ■ ■ , Tn. Matematická logika: H <= T\ a ■ ■ ■ a T, Hana Rudová, Logické programování I, 7. dubna 2009 19 Rezoluce a logické programování Prologovská notace -• Klauzule v matematické logice * {Hi,- ■ ■ ,Hm,-.7i,- ■ ■ ,-.Tn} Hi V ■ ■ ■ vHmV-Ti V ■ ■ ■ v-T, -• Hornova klauzule: nejvýše jeden pozitivní literal * {H,-.Ti,...,-.rn} {H} {-.7i,...,-.rn} -• h v -Ti v ■ ■ ■ v -rn h -Ti v ■ ■ ■ v -rn -• Pravidlo: jeden pozitivní a alespoň jeden negativní literal -• Prolog: H : - T\, ■ ■ ■ , Tn. Matematická logika: H <= T\ a ■ ■ ■ a T, 3 H ^T Hv ->T Hana Rudová, Logické programování I, 7. dubna 2009 19 Rezoluce a logické programování Prologovská notace -• Klauzule v matematické logice * {Hi,- ■ ■ ,Hm,-.7i,- ■ ■ ,-.Tn} Hi V ■ ■ ■ vHmV-Ti V ■ ■ ■ v-T, -• Hornova klauzule: nejvýše jeden pozitivní literal * {H,-.Ti,...,-.rn} {H} {-.7i,...,-.rn} -• h v -Ti v ■ ■ ■ v -rn h -Ti v ■ ■ ■ v -rn -• Pravidlo: jeden pozitivní a alespoň jeden negativní literal -• Prolog: H : - T\, ■ ■ ■ , Tn. Matematická logika: H <= T\ a ■ ■ ■ a T, MH^T Hv^T Hv-ľiV---v-rn Hana Rudová, Logické programování I, 7. dubna 2009 19 Rezoluce a logické programování Prologovská notace -• Klauzule v matematické logice * {Hi,- ■ ■ ,Hm,-.7i,- ■ ■ ,-.Tn} HiV---vHmV-.7iV---V-Tn -• Hornova klauzule: nejvýše jeden pozitivní literal * {H,-.7i,...,-.rn} {H} {-.Ti,...,-.Tn} -• h v -Ti v ■ ■ ■ v -rn h -Ti v ■ ■ ■ v -rn -• Pravidlo: jeden pozitivní a alespoň jeden negativní literal -• Prolog: H : - T\, ■ ■ ■ , Tn. Matematická logika: H <= T\ a ■ ■ ■ a Tn MH^T Hv^T Hv-ľiV---v-rn Klauzule: {fí,-> Ti,...,->Tn} Hana Rudová, Logické programování I, 7. dubna 2009 19 Rezoluce a logické programování Prologovská notace -• Klauzule v matematické logice * {Hi,- ■ ■ ,Hm,-.7i,- ■ ■ ,-.Tn} HiV---vHmV-.7iV---V-Tn -• Hornova klauzule: nejvýše jeden pozitivní literal * {H,-.7i,...,-.rn} {H} {-.Ti,...,-.Tn} -• h v -Ti v ■ ■ ■ v -rn h -Ti v ■ ■ ■ v -rn -• Pravidlo: jeden pozitivní a alespoň jeden negativní literal -• Prolog: H : - T\, ■ ■ ■ , Tn. Matematická logika: H <= T\ a ■ ■ ■ a Tn 3H^T Hv^T Hv-ľiV---v-rn Klauzule: {fí,-> Ti,...,->Tn} -• Fakt: pouze jeden pozitivní literal M Prolog: H. Matematická logika: H Klauzule: {H} Hana Rudová, Logické programování I, 7. dubna 2009 19 Rezoluce a logické programování Prologovská notace -• Klauzule v matematické logice * {Hi,- ■ ■ ,Hm,-.7i,- ■ ■ ,-Tn} HiV---vHmV-.7iV---V-Tn -• Hornova klauzule: nejvýše jeden pozitivní literal * {H,-.7i,...,-.rn} {H} {-.Ti,...,-.Tn} -• h v -Ti v ■ ■ ■ v -rn h -Ti v ■ ■ ■ v -rn -• Pravidlo: jeden pozitivní a alespoň jeden negativní literal -• Prolog: H : - T\, ■ ■ ■ , Tn. Matematická logika: H <= T\ a ■ ■ ■ a Tn 3H^T Hv^T Hv-ľiV---v-rn Klauzule: {ff,-Ti,...,-Tn} -• Fakt: pouze jeden pozitivní literal M Prolog: H. Matematická logika: H Klauzule: {H} M Cílová klauzule: žádný pozitivní literal M Prolog: : - Ti,... Tn. Matematická logika: -Ti v ■ ■ ■ v ^Tn Klauzule: {-Ti, ■ ■ ■ ^Tn} Hana Rudová, Logické programování I, 7. dubna 2009 19 Rezoluce a logické programování Logický program 3 Programová klauzule: právě jeden pozitivní literal (fakt nebo pravidlo) 3 Logický program: konečná množina programových klauzulí .» Príklad: .# logický program jako množina klauzulí: P = {Pl,P2,P3] Pi={p}, P2 = {p,^q}, Ps = {q} Hana Rudová, Logické programování I, 7. dubna 2009 20 Rezoluce a logické programování Logický program M Programová klauzule: právě jeden pozitivní literal (fakt nebo pravidlo) M Logický program: konečná množina programových klauzulí M Príklad: -• logický program jako množina klauzulí: P= {Pl,P2,Ps} Pi = {p}, P2 = {p,^q}, Pi = {q} M logický program v prologovske notaci: P- p: -q. q. 3 cílová klauzule: G = {->g, ->p} : -q, p. Hana Rudová, Logické programování I, 7. dubna 2009 20 Rezoluce a logické programování Lineární rezoluce pro Hornovy klauzule M Začneme s cílovou klauzulí: Q = G M Boční klauzule vybíráme z programových klauzulí P M G= {^q^p} P= {Pi,P2,P3} • Pi = {p}, Pz = {p,^q}, P3 = {q} M :-q,p. p. p--q, q- Hana Rudová, Logické programování I, 7. dubna 2009 21 Rezoluce a logické programování Lineární rezoluce pro Hornovy klauzule 3 Začneme s cílovou klauzulí: Q = G 3 Boční klauzule vybíráme z programových klauzulí P *G={^q,^p} P={P1,P2,P3}: Pi = {p}, P2 = {p,^q}, P3 = iq} -• :-q,p. p. p--q, a- {^q,^p} {q} >'-»< (Pl D Hana Rudová, Logické programování I, 7. dubna 2009 21 Rezoluce a logické programování Lineární rezoluce pro Hornovy klauzule Začneme s cílovou klauzulí: Q = G Boční klauzule vybíráme z programových klauzulí P G = {^q,^p} P= {Pi,P2,P3) ■ Pi = {p}, Pz = {p,^q}, P3 = {q} q,p. P- p: -q, q D {^q,^p} {<Ö {^q^pj {q} {^p} fa^ti {^p} {p} í^qJ (q) D Hana Rudová, Logické programování I, 7. dubna 2009 21 Rezoluce a logické programování Lineární rezoluce pro Hornovy klauzule Začneme s cílovou klauzulí: Q = G Boční klauzule vybíráme z programových klauzulí P G = {^q,^p} P= {Pi,P2,P3) ■ Pi = {p}, Pz = {p,^q}, P3 = {q} q,p. P- p: -q, q D {^q,^p} {<Ö {^q^pj {q} {^p} fa^ti {^p} {p} í^qJ (q) D Střední klauzule jsou cílové klauzule Hana Rudová, Logické programování I, 7. dubna 2009 21 Rezoluce a logické programování Lineární vstupní rezoluce -• Vstupní rezoluce na P u {G} M (opakování:) alespoň jedna z klauzulí použitá při rezoluci je z výchozí vstupní množiny M začneme s cílovou klauzulí: Q = G M boční klauzule jsou vždy z P (tj. jsou to programové klauzule) Hana Rudová, Logické programování I, 7. dubna 2009 22 Rezoluce a logické programování Lineární vstupní rezoluce -• Vstupní rezoluce na P u {G} M (opakování:) alespoň jedna z klauzulí použitá při rezoluci je z výchozí vstupní množiny M začneme s cílovou klauzulí: Q = G M boční klauzule jsou vždy z P (tj. jsou to programové klauzule) M (Opakování:) Lineární rezoluční důkaz C z 5 je posloupnost dvojic {Co,B0), ... {Cn,Bn) taková, že C = Cn+i a M Co a každá Bi jsou prvky S nebo některé Cj,j < í M každá Q+i, í < n je rezolventa Q a £í Hana Rudová, Logické programování I, 7. dubna 2009 22 Rezoluce a logické programování Lineární vstupní rezoluce -• Vstupní rezoluce na P u {G} M (opakování:) alespoň jedna z klauzulí použitá při rezoluci je z výchozí vstupní množiny M začneme s cílovou klauzulí: Co = G M boční klauzule jsou vždy z P (tj. jsou to programové klauzule) M (Opakování:) Lineární rezoluční důkaz C z 5 je posloupnost dvojic {Co,B0), ... {Cn,Bn) taková, že C = Cn+i a M Co a každá Bi jsou prvky S nebo některé Cj,j < í M každá Q+i, í < n je rezolventa Q a £í «• Lineární vstupní (Linear Input) rezoluce (Ll-rezoluce) C z P u {G} posloupnost dvojic {Co,Bo), ... {Cn,Bn) taková, že C = Cn+i a «• Co = G a každá Bi jsou prvky P lineární rezoluce + vstupní rezoluce «• každá Ci+i, í < n je rezolventa Q a Bi Hana Rudová, Logické programování I, 7. dubna 2009 22 Rezoluce a logické programování Cíle a fakta při lineární rezoluci -• Věta:Je-li S nesplnitelná množina Hornovych klauzulí, pak S obsahuje alespoň jeden cíl a jeden fakt. -• pokud nepoužiji cíl, mám pouze fakta (1 požit.literal) a pravidla (1 požit.literal a alespoň jeden negat. literal), při rezoluci mi stále zůstává alespoň jeden požit, literal Hana Rudová, Logické programování I, 7. dubna 2009 23 Rezoluce a logické programování Cíle a fakta při lineární rezoluci -• Věta:Je-li S nesplnitelná množina Hornovych klauzulí, pak S obsahuje alespoň jeden cíl a jeden fakt. -• pokud nepoužiji cíl, mám pouze fakta (1 požit.literal) a pravidla (1 požit.literal a alespoň jeden negat. literal), při rezoluci mi stále zůstává alespoň jeden požit, literal -• pokud nepoužiji fakt, mám pouze cíle (negat.literály) a pravidla (1 požit.literal a alespoň jeden negat. literal), v rezolventě mi stále zůstávají negativní literály Hana Rudová, Logické programování I, 7. dubna 2009 23 Rezoluce a logické programování Cíle a fakta při lineární rezoluci -• Věta:Je-li S nesplnitelná množina Hornovych klauzulí, pak S obsahuje alespoň jeden cíl a jeden fakt. -• pokud nepoužiji cíl, mám pouze fakta (1 požit.literal) a pravidla (1 požit.literal a alespoň jeden negat. literal), při rezoluci mi stále zůstává alespoň jeden požit, literal -• pokud nepoužiji fakt, mám pouze cíle (negat.literály) a pravidla (1 požit.literal a alespoň jeden negat. literal), v rezolventě mi stále zůstávají negativní literály -• Věta: Existuje-li rezoluční důkaz prázdné množiny z množiny S Hornovych klauzulí, pak tento rezoluční strom má v listech jedinou cílovou klauzuli. -• pokud začnu důkaz pravidlem a faktem, pak dostanu zase pravidlo M pokud začnu důkaz dvěma pravidly, pak dostanu zase pravidlo M na dvou faktech rezolvovat nelze Hana Rudová, Logické programování I, 7. dubna 2009 23 Rezoluce a logické programování Cíle a fakta při lineární rezoluci -• Věta:Je-li S nesplnitelná množina Hornovych klauzulí, pak S obsahuje alespoň jeden cíl a jeden fakt. -• pokud nepoužiji cíl, mám pouze fakta (1 požit.literal) a pravidla (1 požit.literal a alespoň jeden negat. literal), při rezoluci mi stále zůstává alespoň jeden požit, literal -• pokud nepoužiji fakt, mám pouze cíle (negat.literály) a pravidla (1 požit.literal a alespoň jeden negat. literal), v rezolventě mi stále zůstávají negativní literály -• Věta: Existuje-li rezoluční důkaz prázdné množiny z množiny S Hornovych klauzulí, pak tento rezoluční strom má v listech jedinou cílovou klauzuli. -• pokud začnu důkaz pravidlem a faktem, pak dostanu zase pravidlo M pokud začnu důkaz dvěma pravidly, pak dostanu zase pravidlo M 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, 7. dubna 2009 23 Rezoluce a logické programování Cíle a fakta při lineární rezoluci -• Věta:Je-li S nesplnitelná množina Hornovych klauzulí, pak S obsahuje alespoň jeden cíl a jeden fakt. -• pokud nepoužiji cíl, mám pouze fakta (1 požit.literal) a pravidla (1 požit.literal a alespoň jeden negat. literal), při rezoluci mi stále zůstává alespoň jeden požit, literal -• pokud nepoužiji fakt, mám pouze cíle (negat.literály) a pravidla (1 požit.literal a alespoň jeden negat. literal), v rezolventě mi stále zůstávají negativní literály -• Věta: Existuje-li rezoluční důkaz prázdné množiny z množiny S Hornovych klauzulí, pak tento rezoluční strom má v listech jedinou cílovou klauzuli. -• pokud začnu důkaz pravidlem a faktem, pak dostanu zase pravidlo M pokud začnu důkaz dvěma pravidly, pak dostanu zase pravidlo M na dvou faktech rezolvovat nelze => dokud nepoužiji cíl pracuji stále s množinou faktů a pravidel -• pokud použiji v důkazu cílovou klauzulí, fakta mi ubírají negat.literály, pravidla mi je přidávají, v rezolventě mám stále samé negativní literály, tj. nelze rezolvovat s dalším cílem Hana Rudová, Logické programování I, 7. dubna 2009 23 Rezoluce a logické programování Korektnost a úplnost -• Věta: Množina S Hornových klauzulí je nesplnitelná, právě když existuje rezoluční vyvrácení S pomocí vstupní rezoluce. M Korektnost platí stejně jako pro ostatní omezení rezoluce -• Úplnost Ll-rezoluce pro Hornovy klauzule: Nechť P je množina programových klauzulí a G cílová klauzule. Je—I i množina P u {G} Hornových klauzulí nesplnitelná, pak existuje rezoluční vyvrácení P u {G} pomocí Ll-rezoluce. * vstupní rezoluce pro (obecnou) formuli sama o sobě není úplná => Ll-rezoluce aplikovaná na (obecnou) formuli nezaručuje, že nalezeneme důkaz, i když formule platí! Hana Rudová, Logické programování I, 7. dubna 2009 24 Rezoluce a logické programování Korektnost a úplnost -• Věta: Množina S Hornových klauzulí je nesplnitelná, právě když existuje rezoluční vyvrácení S pomocí vstupní rezoluce. M Korektnost platí stejně jako pro ostatní omezení rezoluce -• Úplnost Ll-rezoluce pro Hornovy klauzule: Nechť P je množina programových klauzulí a G cílová klauzule. Je—I i množina P u {G} Hornových klauzulí nesplnitelná, pak existuje rezoluční vyvrácení P u {G} pomocí Ll-rezoluce. * vstupní rezoluce pro (obecnou) formuli sama o sobě není úplná => Ll-rezoluce aplikovaná na (obecnou) formuli nezaručuje, že nalezeneme důkaz, i když formule platí! M Význam Ll-rezoluce pro Hornovy klauzule: M P = {Pi,... ,Pn], G = {Gi,..., Gm} M Ll-rezolucí ukážeme nesplnitelnost P\ a ■ ■ ■ a Pn a (->Gi v ■ ■ ■ v ^Gm) Hana Rudová, Logické programování I, 7. dubna 2009 24 Rezoluce a logické programování Korektnost a úplnost -• Věta: Množina S Hornových klauzulí je nesplnitelná, právě když existuje rezoluční vyvrácení S pomocí vstupní rezoluce. M Korektnost platí stejně jako pro ostatní omezení rezoluce -• Úplnost Ll-rezoluce pro Hornovy klauzule: Nechť P je množina programových klauzulí a G cílová klauzule. Je—I i množina P u {G} Hornových klauzulí nesplnitelná, pak existuje rezoluční vyvrácení P u {G} pomocí Ll-rezoluce. * vstupní rezoluce pro (obecnou) formuli sama o sobě není úplná => Ll-rezoluce aplikovaná na (obecnou) formuli nezaručuje, že nalezeneme důkaz, i když formule platí! M Význam Ll-rezoluce pro Hornovy klauzule: M P = {Pi,... ,Pn], G = {Gi,..., Gm} M Ll-rezolucí ukážeme nesplnitelnost P\ a ■ ■ ■ a Pn a (->Gi v ■ ■ ■ v ^Gm) ^ pokud tedy předpokládáme, že program {Pi,... ,Pn} platí, tak musí být nepravdivá (->Gi v ■ ■ ■ v ->Gm), tj. musí platit G\ a ■ ■ ■ a Gm Hana Rudová, Logické programování I, 7. dubna 2009 24 Rezoluce a logické programování