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, 4. dubna 201 2
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, 4. dubna 201 2
2
Rezoluce v PL1
Formule
M literal I
m pozitivní literal = atomická formule p(t\, ■ ■ ■ , tn)
m negativní literal = negace atomické formule ~^p(ti, ■ ■ ■ ,tn)
Hana Rudová, Logické programování I, 4. dubna 201 2
3
Rezoluce v PL1
Formule
-0 literal I
m pozitivní literal = atomická formule p(t\, ■ ■ ■ , tn) m negativní literal = negace atomické formule ->/?(ri, ■ ■ ■ ,tn) M 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)}
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ý literal)
Hana Rudová, Logické programování I, 4. dubna 201 2
3
Rezoluce v PL1
Formule
-0 literál l
m pozitivní literál = atomická formule p(t\, ■ ■ ■ , tn) m negativní literál = negace atomické formule ->/?(ŕi, ■ ■ ■ ,tn) M 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)}
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)
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        A (p v ~^q v r)      notace: {{p,q}, {->p}, {p, ~^q,r}}
Hana Rudová, Logické programování I, 4. dubna 201 2
3
Rezoluce v PL1
Formule
-0 literál l
m pozitivní literál = atomická formule p(t\, ■ ■ ■ , tn) m negativní literál = negace atomické formule ->/?(ŕi, ■ ■ ■ ,tn) M 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)}
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)
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        A (p v ~^q v r)      notace: {{p,q}, {->p}, {p, ~^q,r}}
3 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, 4. dubna 201 2
3
Rezoluce v PL1
Formule
-0 literál l
m pozitivní literál = atomická formule p(t\, ■ ■ ■ , tn) m negativní literál = negace atomické formule ->/?(ŕi, ■ ■ ■ ,tn) M 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)}
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)
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        A (p v ~^q v r)      notace: {{p,q}, {->p}, {p, ~^q,r}}
3 formule je pravdivá <^> všechny klauzule jsou pravdivé
m prázdná formule je vždy pravdivá (neexistuje klauzule, která by byla nepravdivá)
M 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
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, 4. dubna 201 2
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, 4. dubna 201 2
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, 4. dubna 2012 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, 4. dubna 201 2
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
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
Hana Rudová, Logické programování I, 4. dubna 201 2
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
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 5) 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, 4. dubna 201 2
5
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 C/, Ck pro fc, j < i.
Hana Rudová, Logické programování I, 4. dubna 201 2
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, 4. dubna 201 2
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, 4. dubna 201 2
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, 4. dubna 201 2
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}, {^q}}
Ci = ÍP,r} klauzule z F C2 = {q,      klauzule z F C3 = {p, q} rezolventa C\ a C2
Hana Rudová, Logické programování I, 4. dubna 201 2
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, ^r}, {^q}}
Ci = {p,r} klauzule z F C2 = {q, ^r} klauzule z F C3 = rezolventa Ci a C2
C4 = {^g} klauzule z F
Hana Rudová, Logické programování I, 4. dubna 201 2
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
C3 = rezolventa Ci a C2
C4 = {^g} klauzule z F
C5 = {p} = C rezolventa C3 a C4
Hana Rudová, Logické programování I, 4. dubna 201 2
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, 4. dubna 201 2
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, 4. dubna 201 2
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 -iF, musíme postupným uplatňováním rezolučního principu dospět k prázdné klauzuli □
M Příklad:
F...     v a ^F... a a
^F... {{a}, {^a}}
Hana Rudová, Logické programování I, 4. dubna 201 2
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 ~^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 -^F... a a
^F... {{a}, {^a}} Ci = {a},C2 = {^a}
rezolventa C\ a C2 je □, tj. F je vždy pravdivá M rezoluční důkaz □ z formule G se nazývá rezoluční vyvrácení formule G
m a tedy G je nepravdivá ve všech interpretacích, tj. G je nesplnitelná
Hana Rudová, Logické programování I, 4. dubna 2012 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:
3 kořen je označen klauzulí C,
3 listy jsou označeny klauzulemi z F 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: F = {{p,r}, {q, ^r}, {^q}, {^p}} {p,r}    {q,^r} {^q} {^p}
C = □
strom rezolučního vyvrácení
(rezoluční důkaz □ z F)
Hana Rudová, Logické programování I, 4.
dubna 2012
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:
3 kořen je označen klauzulí C,
3 listy jsou označeny klauzulemi z F 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: F = {{p,r}, {q, ^r}, {^q}, {^p}} {p,r}    {q,^r} {^q} {^p}
C = □
príklad: {{p,r}, {q,^r}, {^q}, {->p,t}, {^s}, {s,^t}}
strom rezolučního vyvrácení
(rezoluční důkaz □ z F)
Hana Rudová, Logické programování I, 4.
dubna 2012
8
Rezoluce v PL1