Rezoluce v predikátové logice l.řádu Rezoluce M rezoluční princip: z F v A, G v odvodit F v G M dokazovací metoda používaná v Prologu ve většině systémů pro automatické dokazování Hana Rudová, Logické programování I, 26. března 201 3 2 Rezoluce v PL1 Rezoluce 3 rezoluční princip: z F v A, G v odvodit F v G M dokazovací metoda používaná v Prologu ve většině systémů pro automatické dokazování procedura pro vyvrácení 3 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, 26. března 201 3 2 Rezoluce v PL1 Formule literál l m pozitivní literál = atomická formule p(t\, ■ ■ ■ ,tn) 3 negativní literál = negace atomické formule -"p(ti, ■ ■ ■ ,tn) ti, ■ ■ ■ , tn jsou termy Hana Rudová, Logické programování I, 26. března 201 3 3 Rezoluce v PLI Formule literál l m pozitivní literál = atomická formule p(t\, ■ ■ ■ , tn) m negativní literál = negace atomické formule ->/?(ŕi, ■ ■ ■ ,tn) & t\, ■ ■ ■ , tn jsou termy klauzule C = konečná množina literálů reprezentující jejich disjunkci 3 příklad: p(X) v q{a,f) v ->p(Y) notace: {p{X),q{a,f),^p{Y)} 3 klauzule je pravdivá <^> je pravdivý alespoň jeden z jejích literálů 3 prázdná klauzule se značí □ a je vždy nepravdivá (neexistuje v ní pravdivý literál) Hana Rudová, Logické programování I, 26. března 201 3 3 Rezoluce v PL1 Formule literál l m pozitivní literál = atomická formule p(t\, ■ ■ ■ , tn) m negativní literál = negace atomické formule ->/?(ŕi, ■ ■ ■ ,tn) & t\, ■ ■ ■ , tn jsou termy klauzule C = konečná množina literálů reprezentující jejich disjunkci 3 příklad: p(X) v q{a,f) v ->p(Y) notace: {p{X),q{a,f),^p{Y)} 3 klauzule je pravdivá <^> je pravdivý alespoň jeden z jejích literálů 3 prázdná klauzule se značí □ a je vždy nepravdivá (neexistuje v ní pravdivý literál) M formule F = množina klauzulí reprezentující jejich konjunkci m formule je v tzv. konjuktivní normální formě (konjunkce disjunkcí) 3 příklad: (p v q) A A (p v ~^q v r) notace: {{p,q}, {->p}, {p, ~^q,r}} Hana Rudová, Logické programování I, 26. března 201 3 3 Rezoluce v PL1 Formule literál l m pozitivní literál = atomická formule p(t\, ■ ■ ■ , tn) m negativní literál = negace atomické formule ->/?(ŕi, ■ ■ ■ ,tn) & t\, ■ ■ ■ , tn jsou termy klauzule C = konečná množina literálů reprezentující jejich disjunkci 3 příklad: p(X) v q{a,f) v ->p(Y) notace: {p{X),q{a,f),^p{Y)} 3 klauzule je pravdivá <^> je pravdivý alespoň jeden z jejích literálů 3 prázdná klauzule se značí □ a je vždy nepravdivá (neexistuje v ní pravdivý literál) M formule F = množina klauzulí reprezentující jejich konjunkci m formule je v tzv. konjuktivní normální formě (konjunkce disjunkcí) 3 příklad: (p v q) A A (p v ~^q v r) notace: {{p,q}, {->p}, {p, ~^q,r}} m formule je pravdivá <^> všechny klauzule jsou pravdivé m prázdná formule je vždy pravdivá (neexistuje klauzule, která by byla nepravdivá) Hana Rudová, Logické programování I, 26. března 201 3 3 Rezoluce v PL1 Formule literál l m pozitivní literál = atomická formule p(t\, ■ ■ ■ , tn) m negativní literál = negace atomické formule ->/?(ŕi, ■ ■ ■ ,tn) & t\, ■ ■ ■ , tn jsou termy klauzule C = konečná množina literálů reprezentující jejich disjunkci 3 příklad: p(X) v q{a,f) v ->p(Y) notace: {p{X),q{a,f),^p{Y)} 3 klauzule je pravdivá <^> je pravdivý alespoň jeden z jejích literálů 3 prázdná klauzule se značí □ a je vždy nepravdivá (neexistuje v ní pravdivý literál) M formule F = množina klauzulí reprezentující jejich konjunkci m formule je v tzv. konjuktivní normální formě (konjunkce disjunkcí) 3 příklad: (p v q) A A (p v ~^q v r) notace: {{p,q}, {->p}, {p, ~^q,r}} m formule je pravdivá <^> všechny klauzule jsou pravdivé m prázdná formule je vždy pravdivá (neexistuje klauzule, která by byla nepravdivá) množinová notace: literál je prvek klauzule, klauzule je prvek formule, ... Hana Rudová, Logické programování I, 26. března 201 3 3 Rezoluce v PL1 Splnitelnost [Opakování:] Interpretace 2 jazyka L je dána univerzem T> a zobrazením, které přiřadí konstantě c prvek T>, funkčnímu symbolu f/n n-ární operaci v T> a predikátovému symbolu pln n-ární relaci. 3 příklad: F = {{f(a,b) = f(b,a)}, {f(f(a,a),b) = a}} interpretace li. V = Z, a := l,b := -l,f := " + " Rudová, Logické programování I, 26. března 201 3 4 Rezoluce v PL1 Splnitelnost M [Opakování:] Interpretace 1 jazyka L je dána univerzem T> a zobrazením, které přiřadí konstantě c prvek T>, funkčnímu symbolu f In n-ární operaci v T> a predikátovému symbolu pln n-ární relaci. 3 příklad: F = {{f (a,b) =f(b,a)}, {f (f (a,a),b) = a}} interpretace li. V = Z, a := l,b := -l,f := " + " M Formule je splnitelná, existuje-li interpretace, pro kterou je pravdivá 3 formule je konjunkce klauzulí, tj. všechny klauzule musí být v dané interpretaci pravdivé m příklad (pokrač.): F je splnitelná (je pravdivá v 1\) Hana Rudová, Logické programování I, 26. března 201 3 4 Rezoluce v PL1 Splnitelnost M [Opakování:] Interpretace 1 jazyka L je dána univerzem T> a zobrazením, které přiřadí konstantě c prvek T>, funkčnímu symbolu f In n-ární operaci v T> a predikátovému symbolu pln n-ární relaci. 3 příklad: F = {{f (a,b) =f(b,a)}, {f (f (a,a),b) = a}} interpretace li. V = Z, a := l,b := -l,f := " + " M Formule je splnitelná, existuje-li interpretace, pro kterou je pravdivá 3 formule je konjunkce klauzulí, tj. všechny klauzule musí být v dané interpretaci pravdivé m příklad (pokrač.): F je splnitelná (je pravdivá v 1\) 3 Formule je nesplnitelná, neexistuje-li interpretace, pro kterou je pravdivá 3 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, 26. března 2013 4 Rezoluce v PL1 Rezoluční princip ve výrokové logice Rezoluční princip = pravidlo, které umožňuje odvodit z klauzulí Ci u {1} a {-<ř} u C2 klauzuli C\ u C2 CiuU} W}uC2 Ci u C2 Ci u C2 se nazývá rezolventou původních klauzulí Hana Rudová, Logické programování I, 26. března 201 3 5 Rezoluce v PL1 Rezoluční princip ve výrokové logice M Rezoluční princip = pravidlo, které umožňuje odvodit z klauzulí Ci u {1} a {-<ř} u C2 klauzuli C\ u C2 CiuU} W}uC2 Ci u C2 Ci u C2 se nazývá rezolventou původních klauzulí M příklad: {p,r} {^r,s} (p v r) a (^r v s) {p,s} pvs Hana Rudová, Logické programování I, 26. března 201 3 5 Rezoluce v PL1 Rezoluční princip ve výrokové logice M Rezoluční princip = pravidlo, které umožňuje odvodit z klauzulí Ci u {1} a {-<ř} u C2 klauzuli C\ u C2 Ci u {ž} W}uC2 Ci u C2 M Ci u C2 se nazývá rezolventou původních klauzulí M příklad: {p,r} {^r,s} (p v r) a (^r v s) {p,s} pvs obě klauzule (pvr)a (-ir v s) musí být pravdivé protože r nestačí k pravdivosti obou klauzulí, musí být pravdivé p (pokud je pravdivé -ir) nebo s (pokud je pravdivé r), tedy platí klauzule p v s Hana Rudová, Logické programování I, 26. března 201 3 5 Rezoluce v PL1 Rezoluční důkaz rezoluční důkaz klauzule C z formule F je konečná posloupnost C\ f... f Cfi — d k I auzulí taková, že Q je buď klauzule z F nebo rezolventa C\, Ck pro k,j < i. Hana Rudová, Logické programování I, 26. března 201 3 6 Rezoluce v PL1 Rezoluční důkaz M rezoluční důkaz klauzule C z formule F je konečná posloupnost Ci,..., Cn = C klauzulí taková, že Q je buď klauzule z F nebo rezolventa Q, Ck pro fc, j < i. M příklad: rezoluční důkaz {p} z formule F = {{p,r}, {q, ^r}, {^q}} Hana Rudová, Logické programování I, 26. března 201 3 6 Rezoluce v PLI Rezoluční důkaz M rezoluční důkaz klauzule C z formule F je konečná posloupnost Ci,..., Cn = C klauzulí taková, že Q je buď klauzule z F nebo rezolventa Q, Ck pro fc, j < i. M příklad: rezoluční důkaz {p} z formule F = {{p,r}, {q, ^r}, {^q}} Ci = {p,r} klauzule z F Hana Rudová, Logické programování I, 26. března 201 3 6 Rezoluce v PLI Rezoluční důkaz M rezoluční důkaz klauzule C z formule F je konečná posloupnost Ci,..., Cn = C klauzulí taková, že Q je buď klauzule z F nebo rezolventa Q, Ck pro fc, j < i. M příklad: rezoluční důkaz {p} z formule F = {{p,r}, {q, ^r}, {^q}} Ci = {p,r} klauzule z F C2 = {q, ^r} klauzule z F Hana Rudová, Logické programování I, 26. března 201 3 6 Rezoluce v PLI Rezoluční důkaz rezoluční důkaz klauzule C z formule F je konečná posloupnost Ci,..., Cn = C klauzulí taková, že Q je buď klauzule z F nebo rezolventa Q, Q pro fe, j < í. příklad: rezoluční důkaz {/?} z formule F = {{p,r}, {q, -ir}, {^g}} Ci = {p,r} klauzule z F C2 = {g, ^t} klauzule z F C3 = {p, q} rezolventa C\ a C2 Hana Rudová, Logické programování I, 26. března 201 3 6 Rezoluce v PLI Rezoluční důkaz rezoluční důkaz klauzule C z formule F je konečná posloupnost Ci,..., Cn = C klauzulí taková, že Q je buď klauzule z F nebo rezolventa Q, Ck pro k, j < i. M příklad: rezoluční důkaz {p} z formule F = {{p,r}, {q, ^r}, 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, 26. března 201 3 6 Rezoluce v PLI Rezoluční důkaz rezoluční důkaz klauzule C z formule F je konečná posloupnost Ci,..., Cn = C klauzulí taková, že Q je buď klauzule z F nebo rezolventa Q, Ck pro fe, j < i. M příklad: rezoluční důkaz {p} z formule F = {{p,r}, {q, -ir}, {^q}} Ci = {p,r} klauzule z F C2 = {q, ^r} klauzule z F C3 = rezolventa Ci a C2 C4 = {^g} klauzule z F C5 = {p} = C rezolventa C3 a C4 Hana Rudová, Logické programování I, 26. března 201 3 6 Rezoluce v PLI Rezoluční vyvrácení M důkaz pravdivosti formule F spočívá v demonstraci nesplnitelnosti ^F 3 -iF nesplnitelná => ->F je nepravdivá ve všech interpretacích ^> F je vždy pravdivá Hana Rudová, Logické programování I, 26. března 201 3 7 Rezoluce v PL1 Rezoluční vyvrácení M důkaz pravdivosti formule F spočívá v demonstraci nesplnitelnosti 3 -iF nesplnitelná => ->F je nepravdivá ve všech interpretacích ^> F je vždy pravdivá M 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 □ M Příklad: F... v a Hana Rudová, Logické programování I, 26. března 201 3 7 Rezoluce v PL1 Rezoluční vyvrácení M důkaz pravdivosti formule F spočívá v demonstraci nesplnitelnosti ^F 3 -iF nesplnitelná => ->F je nepravdivá ve všech interpretacích ^> F je vždy pravdivá M začneme-li z klauzulí reprezentujících musíme postupným uplatňováním rezolučního principu dospět k prázdné klauzuli □ M Příklad: F... v a G = ~^F... a a ~^oi G = -*F... {{a}, {^a}} Hana Rudová, Logické programování I, 26. března 201 3 7 Rezoluce v PL1 Rezoluční vyvrácení důkaz pravdivosti formule F spočívá v demonstraci nesplnitelnosti ^F 3 -iF nesplnitelná => ->F je nepravdivá ve všech interpretacích ^ F je vždy pravdivá M začneme-li z klauzulí reprezentujících -iF, musíme postupným uplatňováním rezolučního principu dospět k prázdné klauzuli □ * Příklad: F... v a G = ... a a G = ->F... {{a}, {^a}} Ci = {a},C2 = í^a} rezolventa C\ a C2 je □, tj. F je vždy pravdivá rezoluční důkaz □ z formule G se nazývá rezoluční vyvrácení formule G 3 a tedy G je nepravdivá ve všech interpretacích, tj. G je nesplnitelná Hana Rudová, Logické programování I, 26. března 201 3 7 Rezoluce v PL1 Strom rezolučního důkazu M strom rezolučního důkazu klauzule C z formule G je binární strom: 3 kořen je označen klauzulí C, 3 listy jsou označeny klauzulemi z G a 3 každý uzel, který není listem, St má bezprostředními potomky označené klauzulemi C\ a C2 3 je označen rezolventou klauzulí C\ a C2 M příklad: G = {{p,r}, {q, ^r}, {^q}, {^p}} {p,r} {q,^r} {^q} {^p} C = □ strom rezolučního vyvrácení (rezoluční důkaz □ z G) Hana Rudová, Logické programování I, 26. března 201 3 8 Rezoluce v PL1 Strom rezolučního důkazu M strom rezolučního důkazu klauzule C z formule G je binární strom: 3 kořen je označen klauzulí C, 3 listy jsou označeny klauzulemi z G a 3 každý uzel, který není listem, 3 má bezprostředními potomky označené klauzulemi C\ a C2 3 je označen rezolventou klauzulí C\ a C2 M příklad: G = {{p,r}, {q, ^r}, {^q}, {^p}} {p,r} {q,^r} {^q} {^p} C = □ příklad: {{p,r}, {q,^r}, {^q}, {->p,t}, {^s}, {s,^t}} strom rezolučního vyvrácení (rezoluční důkaz □ z G) Hana Rudová, Logické programování I, 26. března 201 3 8 Rezoluce v PL1 Substituce 3 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 Hana Rudová, Logické programování I, 26. března 201 3 9 Rezoluce v PL1 Substituce 3 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 M substituce je libovolná funkce 0 zobrazující výrazy do výrazů tak, že platí 3 6(E) = E pro libovolnou konstantu E m 6(f(Ei, ■ ■ ■ ,En)) = f(6(Ei), ■ ■ ■ , 6(En)) pro libovolný funkční symbol / * 6(p(Ei, ■ ■ ■ ,En)) = p(6(Ei), ■ ■ ■ , 6(En)) pro libovolný predik. symbol p substituce je tedy homomorfismus výrazů, který zachová vše kromě proměnných - ty lze nahradit čímkoliv M substituce zapisujeme zpravidla ve tvaru seznamu [Xi/^i, ■ ■ ■ ,Xn/^n] kde Xi jsou proměnné a 5í substituované termy m příklad: p(X)[X/f(a)] = p(f(a)) Hana Rudová, Logické programování I, 26. března 201 3 9 Rezoluce v PL1 Substituce 3 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 M substituce je libovolná funkce 0 zobrazující výrazy do výrazů tak, že platí 3 6(E) = E pro libovolnou konstantu E m 6(f(Ei, ■ ■ ■ ,En)) = f(6(Ei), ■ ■ ■ , 6(En)) pro libovolný funkční symbol / * 6(p(Ei, ■ ■ ■ ,En)) = p(6(Ei), ■ ■ ■ , 6(En)) pro libovolný predik. symbol p substituce je tedy homomorfismus výrazů, který zachová vše kromě proměnných - ty lze nahradit čímkoliv M substituce zapisujeme zpravidla ve tvaru seznamu [Xi/^i, ■ ■ ■ ,Xn/^n] kde Xi jsou proměnné a 5í substituované termy m příklad: p(X)[X/f(a)] = p(f(a)) M přejmenování proměnných: speciální náhrada proměnných proměnnými m příklad: p{X)[X/Y] = p{Y) Hana Rudová, Logické programování I, 26. března 201 3 9 Rezoluce v PL1 Unifikace Ztotožnění dvou literálů p, q pomocí vhodné substituce a(fc), ^a{Z)} v jednom kroku potřebuji vyrezolvovat zároveň b\ i b2 Hana Rudová, Logické programování I, 26. března 201 3 Rezoluce v PL1 Rezoluce v PLI M Obecný rezoluční princip v PL1 Ci u {Ai, ■ ■ ■ , Am} {^£1, ■ ■ ■ , ^Bn} u C2 Cipa u C2a(fc), ^a{Z)} v jednom kroku potřebuji vyrezolvovat zároveň b\ i b2 M Rezoluce v PL1 3 korektní: jestliže existuje rezoluční vyvrácení F, pak F je nesplnitelná m úplná: jestliže F je nesplnitelná, pak existuje rezoluční vyvrácení F Hana Rudová, Logické programování I, 26. března 201 3 Rezoluce v PL1 Zefektivnění rezoluce M rezoluce je intuitivně efektivnější než axiomatické systémy axiomatické systémy: který z axiomů a pravidel použít? m rezoluce: pouze jedno pravidlo Hana Rudová, Logické programování I, 26. března 201 3 14 Rezoluce v PL1 Zefektivnění rezoluce M rezoluce je intuitivně efektivnější než axiomatické systémy 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í M strategie pro zefektivnění prohledávání => varianty rezoluční metody Hana Rudová, Logické programování I, 26. března 201 3 14 Rezoluce v PL1 Zefektivnění rezoluce M rezoluce je intuitivně efektivnější než axiomatické systémy 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í M strategie pro zefektivnění prohledávání => varianty rezoluční metody M vylepšení prohledávání zastavit prohledávání cest, které nejsou slibné specifikace pořadí, jak procházíme alternativními cestami Hana Rudová, Logické programování I, 26. března 201 3 14 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í Hana Rudová, Logické programování I, 26. března 201 3 1 5 Rezoluce v PL1 Varianty rezoluční metody M Věta: Každé omezení rezoluce je korektní. 3 stále víme, že to, co jsme dokázali, platí M T-rezoluce: klauzule účastnící se rezoluce nejsou tautologie úplná 3 tautologie nepomůže ukázat, že formule je nesplnitelná Hana Rudová, Logické programování I, 26. března 201 3 Rezoluce v PL1 Varianty rezoluční metody M Věta: Každé omezení rezoluce je korektní. m stále víme, že to, co jsme dokázali, platí M T-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ň jedna je v této interpretaci nepravdivá m pokud jsou obě klauzule pravdivé, těžko odvodíme nesplnitelnost formule Hana Rudová, Logické programování I, 26. března 201 3 Rezoluce v PL1 Varianty rezoluční metody M Věta: Každé omezení rezoluce je korektní. m stále víme, že to, co jsme dokázali, platí M T-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ň jedna je 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, 26. března 201 3 Rezoluce v PL1 Varianty rezoluční metody 3 Věta: Každé omezení rezoluce je korektní. 3 stále víme, že to, co jsme dokázali, platí T-rezoluce: klauzule účastnící se rezoluce nejsou tautologie úplná m tautologie nepomůže ukázat, že formule je nesplnitelná M 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 vstupní (input) rezoluce: neúplná alespoň jedna z klauzulí, použitá při rezoluci, je z výchozí vstupní množiny S 3 {{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, 26. března 2013 15 Rezoluce v PL1