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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010                          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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010                          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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010                         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, 8. dubna 2010                          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
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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010                         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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010                          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, 8. dubna 2010
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, 8. dubna 2010                          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, 8. dubna 2010                          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
<M je označen rezolventou klauzulí C\ a C2
-• příklad: F = {{p,r}, {g, ^r}, {^g}, {^p}}        C = D {p,r}     {q,^r}   {^q}       {^p}
strom rezolučního vyvrácení
(rezoluční důkaz D z i7)
Hana Rudová, Logické programování I, 8. dubna 2010
8
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
<M je označen rezolventou klauzulí C\ a C2
-• příklad: F = {{p,r}, {g, ^r}, {^g}, {^p}}        C = D {p,r}     {q,^r}   {^q}       {^p}
strom rezolučního vyvrácení
(rezoluční důkaz D z i7)
u                         príklad: {{p,r], {q,^r}, {^q}, {--p,t}, {^s}, {s,^ŕ}}
Hana Rudová, Logické programování I, 8. dubna 2010                         8                                                                                              Rezoluce v PLI
Substituce
J cos 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, 8. dubna 2010                         9                                                                                              Rezoluce v PL1
Substituce
J cos 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
-• substituce je libovolná funkce 0 zobrazující výrazy do výrazů tak, že platí
.# 0(E) = E pro libovolnou konstantu E
M 6(f (E\, ■ ■ ■ ,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
M substituce je tedy homomorfismus výrazů, který zachová vše kromě proměnných - ty lze nahradit čímkoliv
-• substituce zapisujeme zpravidla ve tvaru seznamu [Xi/ši, ■ ■ ■ ,Xn/^n] kde Xi jsou proměnné a £í substituované termy
*   příklad:        p(X)[X/f(a)] = p(f(a))
Hana Rudová, Logické programování I, 8. dubna 2010
9
Rezoluce v PL1
Substituce
J cos 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
-• substituce je libovolná funkce 0 zobrazující výrazy do výrazů tak, že platí
.# 0(E) = E pro libovolnou konstantu E
M 6(f (E\, ■ ■ ■ ,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
M substituce je tedy homomorfismus výrazů, který zachová vše kromě proměnných - ty lze nahradit čímkoliv
-• substituce zapisujeme zpravidla ve tvaru seznamu [Xi/ši, ■ ■ ■ ,Xn/^n] kde Xi jsou proměnné a £í substituované termy
*   příklad:        p(X)[X/f(a)] = p(f(a))
3 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, 8. dubna 2010                         9                                                                                              Rezoluce v PL1
Unifikace
-• Ztotožnění dvou literálu p, q pomocí vhodné substituce <x takové, že pa = qa nazýváme unifikácia příslušnou substituci unifikátorem.
M Unifikátorem množiny S literálu nazýváme substituce 0 takovou, že množina
se = {te\t g s]
má jediný prvek.
Hana Rudová, Logické programování I, 8. dubna 2010
10
Rezoluce v PL1
Unifikace
-• Ztotožnění dvou literálu p, q pomocí vhodné substituce <x takové, že pa = qa nazýváme unifikácia příslušnou substituci unifikátorem.
M Unifikátorem množiny S literálu nazýváme substituce 0 takovou, že množina
se = {te\t g s]
má jediný prvek.
M  příklad: 5 = { datum( Dl, Ml, 2003 ), datum( 1, M2, Y2) }
unifikátor 0 = [Dl/1, Ml/2, M2/2, Y2/2003]                              S6 = { datum( 1, 2, 2003 ) }
Hana Rudová, Logické programování I, 8. dubna 2010
10
Rezoluce v PL1
Unifikace
-• Ztotožnění dvou literálu p, q pomocí vhodné substituce <x takové, že pa = qa nazýváme unifikácia příslušnou substituci unifikátorem.
M Unifikátorem množiny S literálu nazýváme substituce 0 takovou, že množina
se = {te\t g s]
má jediný prvek.
M  příklad: 5 = { datum( Dl, Ml, 2003 ), datum( 1, M2, Y2) }
unifikátor 0 = [Dl/1, Ml/2, M2/2, Y2/2003]                              SO = { datum( 1, 2, 2003 ) }
M Unifikátor a množiny S nazýváme nejobecnějším unifikátorem (mgu - most
general unifier), jestliže pro libovolný unifikátor 0 existuje substituce A taková, že 0 = <tA.
Hana Rudová, Logické programování I, 8. dubna 2010
10
Rezoluce v PL1
Unifikace
-• Ztotožnění dvou literálu p, q pomocí vhodné substituce <x takové, že pa = qa nazýváme unifikácia příslušnou substituci unifikátorem.
M Unifikátorem množiny S literálu nazýváme substituce 0 takovou, že množina
se = {te\t g s]
má jediný prvek.
M  příklad: 5 = { datum( Dl, Ml, 2003 ), datum( 1, M2, Y2) }
unifikátor 0 = [Dl/1, Ml/2, M2/2, Y2/2003]                              SO = { datum( 1, 2, 2003 ) }
M Unifikátor a množiny S nazýváme nejobecnějším unifikátorem (mgu - most
general unifier), jestliže pro libovolný unifikátor 0 existuje substituce A taková, že 0 = <tA.
M příklad (pokrač.): nejobecnější unifikátor <j = [Dl/1, Y2/2003, M1/M2],
Hana Rudová, Logické programování I, 8. dubna 2010
10
Rezoluce v PL1
Unifikace
-• Ztotožnění dvou literálu p, q pomocí vhodné substituce <x takové, že pa = qa nazýváme unifikácia příslušnou substituci unifikátorem.
M Unifikátorem množiny S literálu nazýváme substituce 0 takovou, že množina
se = {te\t g s]
má jediný prvek.
M  příklad: 5 = { datum( Dl, Ml, 2003 ), datum( 1, M2, Y2) }
unifikátor 0 = [Dl/1, Ml/2, M2/2, Y2/2003]                              SO = { datum( 1, 2, 2003 ) }
M Unifikátor a množiny S nazýváme nejobecnějším unifikátorem (mgu - most
general unifier), jestliže pro libovolný unifikátor 0 existuje substituce A taková, že 0 = <tA.
M  příklad (pokrač.): nejobecnější unifikátor a = [Dl/1, Y2/2003, M1/M2],       A=[M2/2]
Hana Rudová, Logické programování I, 8. dubna 2010
10
Rezoluce v PL1
Rezoluční princip v PL1
základ:
M rezoluční princip ve výrokové logice----------------------------------
Ci u C2
M substituce, unifikátor, nejobecnější unifikátor
Hana Rudová, Logické programování I, 8. dubna 2010                        11                                                                                              Rezoluce v PL1
Rezoluční princip v PLl
základ:
M rezoluční princip ve výrokové logice----------------------------------
Ci u C2
M substituce, unifikátor, nejobecnější unifikátor
rezoluční princip v PLl je pravidlo, které
-• připraví příležitost pro uplatnění vlastního rezolučního pravidla nalezením vhodného unifikátoru
-• provede rezoluci a získá rezolventu
Hana Rudová, Logické programování I, 8. dubna 2010                        11                                                                                              Rezoluce v PLl
Rezoluční princip v PL1
základ:
M rezoluční princip ve výrokové logice----------------------------------
C-l u C2
M substituce, unifikátor, nejobecnější unifikátor
rezoluční princip v PL1 je pravidlo, které
-• připraví příležitost pro uplatnění vlastního rezolučního pravidla nalezením vhodného unifikátoru
-• provede rezoluci a získá rezolventu
CiU{A}              H}uC2
C\p(j u C2Ö"
M kde p je přejmenováním proměnných takové,
že klauzule (Ci u A)p a {5} u C2 nemají společné proměnné
••   a je nejobecnější unifikátor klauzulí Ap a ß
Hana Rudová, Logické programování I, 8. dubna 2010
1 1
Rezoluce v PL1
Príklad: rezoluce v PLI
* příklad: d = íp(X,Y),    q(Y)}       C2 = í^q(a),    s(X,W)}
Hana Rudová, Logické programování I, 8. dubna 2010                        12                                                                                             Rezoluce v PLI
Príklad: rezoluce v PLI
* příklad: d = íp(X,Y),    q(Y)}       C2 = {^q(a),    s(X,W)}
M přejmenování proměnných: p = [XIZ]
d = {p(Z,Y),    q(Y)}       C2 = í^q(a),    s(X,W)}
Hana Rudová, Logické programování I, 8. dubna 2010
12
Rezoluce v PLI
Príklad: rezoluce v PLI
* příklad: d = íp(X,Y),    q(Y)}       C2 = {^q(a),    s(X,W)}
M přejmenování proměnných: p = [XIZ]
d = {p(Z,Y),    q(Y)}       C2 = {^q(a),    s(X,W)}
-• nejobecnější unifikátor: cr = [Y/a]
Ci = {p(Z,a),    q(a)}       C2 = {^q(a),    s(X,W)}
Hana Rudová, Logické programování I, 8. dubna 2010
12
Rezoluce v PLI
Příklad: rezoluce v PLl
3 příklad: Ci = {p(X,Y),    q(Y)}       C2 = {^q(a),    s(X,W)}
M přejmenování proměnných: p = [XIZ]
d = {p(Z,Y),    q(Y)}       C2 = {^q(a),    s(X,W)}
M nejobecnější unifikátor: <x = [Y/a]
Ci = {p(Z,a),    q(a)}       C2 = {^q(a),    s(X,W)}
M rezoluční princip: C = {p(Z,a),    s(X,W)}
Hana Rudová, Logické programování I, 8. dubna 2010                        12                                                                                             Rezoluce v PLl
Príklad: rezoluce v PLI
* příklad: d = íp(X,Y),    q(Y)}       C2 = {^q(a),    s(X,W)}
M přejmenování proměnných: p = [XIZ]
d = {p(Z,Y),    q(Y)}       C2 = {^q(a),    s(X,W)}
-• nejobecnější unifikátor: a = [Y/a]
Ci = {p(Z,a),    q(a)}       C2 = {^q(a),    s(X,W)}
■M rezoluční princip: C = {p(Z,a),    s(X, W)}
-• vyzkoušejte si:
d = {q(X),    -.r (F),    p(X,Y),    p(/(Z),/(Z))}
C2 = {n(Y),    --r (WO,    -.p(/(a),/(a)),    -.p(/(WO,/(WO}
Hana Rudová, Logické programování I, 8. dubna 2010                        12                                                                                             Rezoluce v PLI
Rezoluce v PLI
-• Obecný rezoluční princip v PLl
Ci u {Ai, ■ ■ ■ , Am}            {-"fli, ■ ■ ■ , ^Bn} u C2
C\p(j u C2Ö"
M kde p je přejmenováním proměnných takové, že množiny klauzulí
{Aip, ■ ■ ■ ,Amp, Cíp} a {Bi, ■ ■ ■ ,Bn, C2} nemají společné proměnné
3   a je nejobecnější unifikátor množiny {Aip, ■ ■ ■ ,Amp,Bi, ■ ■ ■ ,Bn}
Hana Rudová, Logické programování I, 8. dubna 2010
13
Rezoluce v PLl
Rezoluce v PLI
-• Obecný rezoluční princip v PL1
Ci u {Ai, ■ ■ ■ , Am}             {-"fli, ■ ■ ■ , ^Bn} u C2
C\p(j u C2Ö"
M kde p je přejmenováním proměnných takové, že množiny klauzulí
{Aip, ■ ■ ■ ,Amp, Cíp} a {Bi, ■ ■ ■ ,Bn, C2} nemají společné proměnné
3   a je nejobecnější unifikátor množiny {Aip, ■ ■ ■ ,Amp,Bi, ■ ■ ■ ,Bn}
M příklad: Ax = a(X) vs. {^Bu ^B2} = í^a(b), ^a(Z)}
v jednom kroku potřebuji vyrezolvovat zároveň B\ i B2
Hana Rudová, Logické programování I, 8. dubna 2010
13
Rezoluce v PL1
Rezoluce v PLI
-• Obecný rezoluční princip v PL1
Ci u {Ai, ■ ■ ■ , Am}             {-"fli, ■ ■ ■ , ^Bn} u C2
C\p(j u C2Ö"
M kde p je přejmenováním proměnných takové, že množiny klauzulí
{Aip, ■ ■ ■ ,Amp, Cíp} a {Bi, ■ ■ ■ ,Bn, C2} nemají společné proměnné
3   a je nejobecnější unifikátor množiny {Aip, ■ ■ ■ ,Amp,Bi, ■ ■ ■ ,Bn}
M příklad: Ax = a(X) vs. {^Bu ^B2} = í^a(b), ^a(Z)}
v jednom kroku potřebuji vyrezolvovat zároveň B\ i B2
M Rezoluce v PL1
-• korektní: jestliže existuje rezoluční vyvrácení i7, pak i7 je nesplnitelná M úplná: jestliže i7 je nesplnitelná, pak existuje rezoluční vyvrácení i7
Hana Rudová, Logické programování I, 8. dubna 2010
13
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
Hana Rudová, Logické programování I, 8. dubna 2010                        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
Hana Rudová, Logické programování I, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010                        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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010                        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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 201 0                        1 9                                                             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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 201 0                        1 9                                                             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, 8. dubna 201 0                        1 9                                                             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, 8. dubna 2010
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, 8. dubna 2010                        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, 8. dubna 2010
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
{^q^pj   {q}
D
Hana Rudová, Logické programování I, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010                        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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010                        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, 8. dubna 2010
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, 8. dubna 2010
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, 8. dubna 2010                        24                                                             Rezoluce a logické programování