Rezoluce Rezoluce v predikátové logice l.řádu ■ rezoluční princip: z F v A, G v ->A odvodit F v 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á Formule literál / ■ pozitivní literál = atomická formule p(h, ■ ■ ■ ,tn) ■ negativní literál = negace atomické formule ->p(t\, ■ ■ ■ ,tn) klauzule C = konečná množina literálů reprezentující jejich disjunkci ■ příklad: p(X) v q(a,f) v -ip(Y) notace: {p(X),q(a,f),-ip(Y)} ■ klauzule je pravdivá je pravdivý alespoň jeden z jejích literálů ■ prázdná klauzule se značí □ aje 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 v q) a (-ip) a (p v -iq v 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, 4. dubna 2012 3 Rezoluce v PL1 Hana Rudová, Logické programování I, 4. dubna 2012 2 Rezoluce v PL1 Splnitelnost ■ [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 p In n-ární relaci. ■ příklad: F = {{f(a,b)=f(b,a)}, {f(f(a,a),b) = a}} interpretace 1\. D = Z,a:= l,b := -1,/ := " + " ■ 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 'h) ■ 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(«)}} je nesplnitelná ({p(a)\ a {-ip(a)} nemohou být zároveň pravdivé) Hana Rudová, Logické programování I, 4. dubna 2012 4 Rezoluce v PL1 Rezoluční princip ve výrokové logice Rezoluční důkaz Rezoluční princip = pravidlo, které umožňuje odvodit z klauzulí d u {1} a {-ii} u C2 klauzuli C\ u C2 Ciujil HluC2 CiuC2 Ci u C2 se nazývá rezolventou původních klauzulí příklad: {p,r} {^r,s} (p v r) a (-if v í) {p,s} p v s obě klauzule (pvr)a (-ir v 5) musí být pravdivé protože r nestačí k pravdivosti obou klauzulí, musí být pravdivé p (pokud je pravdivé - -iF je nepravdivá ve všech interpretacích => F je vždy pravdivá 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 ... -ifl v a -i F ... a a -ifl -■F...{{«},{-«}} Ci = {fl},C2 = {-ia} rezolventa Ci 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 ■ a tedy C je nepravdivá ve všech interpretacích, tj. C je nesplnitelná Hana Rudová, Logické programování I, 4. dubna 2012 7 Rezoluce v PL1 Hana Rudová, Logické programování I, 4. dubna 2012 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 Q a C2 ■ je označen rezolventou klauzulí C\ a Ci ■ příklad: F = {{p,r}, {q, -*r}, {^q}, {^p}} C = D {p,r} {q,^r} {^q} {^p} strom rezolučního vyvrácení (rezoluční důkaz □ z F) příklad: {{p,r}, {q, ^r}, {^q}, {^p, t}, {^s}, {s, ^ŕ}} Hana Rudová, Logické programování I, 4. dubna 201 2 Rezoluce v PLI