Negace v logickém programování
Negativní znalost
M logické programy vyjadřují pozitivní znalost
-• negativní literály: pozice určena definicí Hornových klauzulí => nelze vyvodit negativní informaci z logického programu
M každý predikát definuje úplnou relaci
«• negativní literal není logickým důsledkem programu
Hana Rudová, Logické programování I, 14. dubna 2009                       2                                                              Negace v logickém programování
Negativní znalost
M logické programy vyjadřují pozitivní znalost
-• negativní literály: pozice určena definicí Hornových klauzulí => nelze vyvodit negativní informaci z logického programu
M každý predikát definuje úplnou relaci
«• negativní literal není logickým důsledkem programu
-• relace vyjádřeny explicitně v nejmenším Herbrandove modelu
M nad(X,Y) : -na(X,Y).                             na(c,b).
nad(X, Y) : -na(X, Z),nad(Z, Y).             na(b, a).
* nejmenší Herbranduv model: {na(b,a),na(c, b),nad(b,a),nad(c, b),nad(c,a)}
Hana Rudová, Logické programování I, 14. dubna 2009
2
Negace v logickém programování
Negativní znalost
M logické programy vyjadřují pozitivní znalost
-• negativní literály: pozice určena definicí Hornových klauzulí => nelze vyvodit negativní informaci z logického programu
M každý predikát definuje úplnou relaci
«• negativní literal není logickým důsledkem programu
-• relace vyjádřeny explicitně v nejmenším Herbrandove modelu
M nad(X,Y) : -na(X,Y).                             na(c,b).
nad(X, Y) : -na(X, Z),nad(Z, Y).             na(b, a).
* nejmenší Herbranduv model: {na(b,a),na(c, b),nad(b,a),nad(c, b),nad(c,a)}
M ani program ani model nezahrnují negativní informaci
-• a není nad c, a není na c
M i v realitě je negativní informace vyjádřena explicitně zřídka, např. jízdní řád
Hana Rudová, Logické programování I, 14. dubna 2009
2
Negace v logickém programování
Předpoklad uzavřeného světa
-• neexistence informace chápána jako opak:
předpoklad uzavřeného světa (dosed world assumption, CWA)
-• převzato z databází
-• určitý vztah platí pouze když je vyvoditelný z programu.
P \£ A & „odvozovací pravidlo" (A je (uzavřený) term):------—        (CWA)
Hana Rudová, Logické programování I, 14. dubna 2009
3
Negace v logickém programování
Předpoklad uzavřeného světa
-• neexistence informace chápána jako opak:
předpoklad uzavřeného světa (dosed world assumption, CWA)
-• převzato z databází
-• určitý vztah platí pouze když je vyvoditelný z programu.
P \£ A & „odvozovací pravidlo" (A je (uzavřený) term):-----—        (CWA)
->A
-• pro SLD-rezoluci: P \£ nad(a,c), tedy lze podle CWA odvodit ^nad(a,c)
Hana Rudová, Logické programování I, 14. dubna 2009
3
Negace v logickém programování
Předpoklad uzavřeného světa
-• neexistence informace chápána jako opak:
předpoklad uzavřeného světa (dosed world assumption, CWA)
-• převzato z databází
-• určitý vztah platí pouze když je vyvoditelný z programu.
P \£ A & „odvozovací pravidlo" (A je (uzavřený) term):-----—        (CWA)
->A
-• pro SLD-rezoluci: P \£ nad(a,c), tedy lze podle CWA odvodit ^nad(a,c)
M problém: není rozhodnutelné, zda daná atomická formule je logickým důsledkem daného logického programu.
M nelze tedy určit, zda pravidlo CWA je aplikovatelné nebo ne M CWA v logickém programování obecně nepoužitelná.
Hana Rudová, Logické programování I, 14. dubna 2009
3
Negace v logickém programování
Negace jako neúspěch (negation as failure)
slabší verze CWA: definitivně neúspěšný (finitely failed) SLD-strom cíle : -A : -A má definitivně (konečně) neúspěšný SLD-strom
-A normální cíl: cíl obsahující i negativní literály
-• :-nad(c,a), ^nad(b,c).
(negation as failure, NF)
Hana Rudová, Logické programování I, 14. dubna 2009
4
Negace v logickém programování
Negace jako neúspěch (negation as failure)
slabší verze CWA: definitivně neúspěšný (finitely failed) SLD-strom cíle : -A
: -A má definitivně (konečně) neúspěšný SLD-strom       ,           .            . .. --------------------------------------------------------------------------       (negation as failure, NF)
normální cíl: cíl obsahující i negativní literály -• :-nad(c,a),->nad(b,c).
rozdíl mezi CWA a NF
-• program    nad(X,Y) : -nad(X,Y), cíl     : -^nad(b,c)
M neexistuje odvození cíle podle NF, protože SLD-strom : -nad(b,c) je nekonečný
-• existuje odvození cíle podle CWA, protože neexistuje vyvrácení: -nad(b,c)
Hana Rudová, Logické programování I, 14. dubna 2009
4
Negace v logickém programování
Negace jako neúspěch (negation as failure)
slabší verze CWA: definitivně neúspěšný (finitely failed) SLD-strom cíle : -A
: -A má definitivně (konečně) neúspěšný SLD-strom       ,           .            . .. --------------------------------------------------------------------------       (negation as failure, NF)
normální cíl: cíl obsahující i negativní literály -• :-nad(c,a),->nad(b,c).
rozdíl mezi CWA a NF
-• program    nad(X,Y) : -nad(X,Y), cíl     : -^nad(b,c)
M neexistuje odvození cíle podle NF, protože SLD-strom : -nad(b,c) je nekonečný
-• existuje odvození cíle podle CWA, protože neexistuje vyvrácení: -nad(b,c)
CWA i NF jsou nekorektní: A není logickým důsledkem programu P
řešení: definovat programy tak, aby jejich důsledkem byly i negativní literály zúplnění logického programu
Hana Rudová, Logické programování I, 14. dubna 2009
4
Negace v logickém programování
Podstata zúplnění logického programu
-• převod všech if příkazů v logickém programu na iff
3 nad(X,Y) : -na(X,Y).
nad(X,Y) : -na(X,Z),nad(Z,Y).
3 lze psát jako: nad(X,Y) : -(na(X,Y)) v (na(X,Z),nad(Z,Y)).
M zúplnění: nad(X,Y) ++ (na(X,Y)) v (na(X,Z),nad(Z,Y)).
Hana Rudová, Logické programování I, 14. dubna 2009
5
Negace v logickém programování
Podstata zúplnění logického programu
-• převod všech if příkazů v logickém programu na iff
3 nad(X,Y) : -na(X,Y).
nad(X,Y) : -na(X,Z),nad(Z,Y).
3 lze psát jako: nad(X,Y) : -(na(X,Y)) v (na(X,Z),nad(Z,Y)).
M zúplnění: nad(X,Y) ++ (na(X,Y)) v (na(X,Z),nad(Z,Y)).
M X je nad Y právě tehdy, když alespoň jedna z podmínek platí
M tedy pokud žádná z podmínek neplatí, X není nad Y
Hana Rudová, Logické programování I, 14. dubna 2009
5
Negace v logickém programování
Podstata zúplnění logického programu
-• převod všech if příkazů v logickém programu na iff
3 nad(X,Y) : -na(X,Y).
nad(X,Y) : -na(X,Z),nad(Z,Y).
3 lze psát jako: nad(X,Y) : -(na(X,Y)) v (na(X,Z),nad(Z,Y)).
M zúplnění: nad(X,Y) ++ (na(X,Y)) v (na(X,Z),nad(Z,Y)).
M X je nad Y právě tehdy, když alespoň jedna z podmínek platí
M tedy pokud žádná z podmínek neplatí, X není nad Y
M kombinace klauzulí je možná pouze pokud mají identické hlavy
M na(c,b). na(b,a).
M lze psát jako: na(Xi,X2) : -X\ = c,X2 = b.
na(Xi,X2) : -X\ = b,X2 = a.
S zúplnění: na(Xi,X2) \-(X\ = c,X2 = b) v (X\ = b,X2 = a).
Hana Rudová, Logické programování I, 14. dubna 2009                       5                                                              Negace v logickém programování
Zúplnění programu
-• Zúplnění programu P je: comp(P) := IFF(P) u CET
-• Základní vlastnosti:
M comp (P) i= P
-• do programuje přidána pouze negativní informace
Hana Rudová, Logické programování I, 14. dubna 2009
6
Negace v logickém programování
Zúplnění programu
-• Zúplnění programu P je: comp(P) := IFF(P) u CET
-• Základní vlastnosti:
M comp (P) i= P
-• do programuje přidána pouze negativní informace
M IFF(P): spojka : - v IF(P) je nahrazena spojkou <-
M IF(P): množina všech formulí IF(g,P)
pro všechny predikátové symboly q v programu P
-• def(p/n) predikátu pln množina všech klauzulí predikátu pln
Hana Rudová, Logické programování I, 14. dubna 2009
6
Negace v logickém programování
IF(4,P)
na(Xi,X2) : -3Y(X1 = c,X2 = b,f(Y)) v (Xľ = b,X2 = a,g). q/n predikátový symbol programu P                    na(c,b) :-f(Y).   na(b,a): -g.
X\,... ,Xn jsou „nové" proměnné, které se nevyskytují nikde v P
Nechť C je klauzule ve tvaru
q{ti,... ,tn) . —Li,...,Lm
kde m > 0, ti,..., tn jsou termy a Li,... ,Lm jsou literály.
Pak označme E(C) výraz 3Y\,..., Yk(X\ = ti,...,Xn = tn,Li,... ,Lm) kde Yi,...,Y]c jsou všechny proměnné v C.
Hana Rudová, Logické programování I, 14. dubna 2009
7
Negace v logickém programování
IF(4,P)
na(Xi,X2) : -3Y(X1 = c,X2 = b,f(Y)) v (Xľ = b,X2 = a,g). q/n predikátový symbol programu P                    na(c,b) :-f(Y).   na(b,a): -g.
X\,... ,Xn jsou „nové" proměnné, které se nevyskytují nikde v P
Nechť C je klauzule ve tvaru
q{ti,... ,tn) . —Li,...,Lm
kde m > 0, ti,..., tn jsou termy a Li,... ,Lm jsou literály.
Pak označme E(C) výraz 3Y\,..., Yk(X\ = ti,...,Xn = tn,Li,... ,Lm) kde Yi,...,Y]c jsou všechny proměnné v C.
Nechť def(q/n) = {Ci,..., Cn}.
Pak formuli l¥(q,P) získáme následujícím postupem:
q(Xi, ...,Xn): -HCi) v E(C2) v ■ ■ ■ v E(Cj)   pro j > 0 a
í|(Xi, ... ,Xn) :                                                      pro j = 0 [q/n není v programu P]
Hana Rudová, Logické programování I, 14. dubna 2009
7
Negace v logickém programování
Čiarková Teorie Rovnosti (CET)
všechny formule jsou univerzálně kvantifikovány: ].X = X
2.X =Y - y = X 3.X =Y AY = Z ^ X = Z
4.  pro každý f/m: Xľ = Yľ a ■ ■ ■ a Xm = Ym - f(Xu ... ,Xm) = f(Yu...,Ym)
5.  pro každý p/m: Xi = Yi a ■ ■ ■ a Xm = Ym - (p(Xi,...,Xm) - p(Yi,...,Ym))
6.  pro všechny různé f Im a gin, {m,n > 0): f(Xi,... ,Xm) =/= g(Yi,..., Yn)
7.  pro každý f/m: f(Xl,...,Xm) = f(Yl,..., Ym) - Xľ = Yľ a ■ ■ ■ AXm = Ym
8.  pro každý term t obsahující X jako vlastní podterm: t =/= X
X 41 Y je zkrácený zápis ->(X = Y)
Hana Rudová, Logické programování I, 14. dubna 2009
8
Negace v logickém programování
Korektnost a úplnost NF pravidla
«• Korektnost NF pravidla: Nechť P logický program a : -A cíl. Jestliže : -A má definitivně neúspěšný SLD-strom, pak V(->A) je logickým důsledkem comp(P) (nebo-li comp(P) i= V(->A))
Hana Rudová, Logické programování I, 14. dubna 2009                       9                                                              Negace v logickém programování
Korektnost a úplnost NF pravidla
«• Korektnost NF pravidla: Nechť P logický program a : -A cíl. Jestliže : -A má definitivně neúspěšný SLD-strom, pak V(->A) je logickým důsledkem comp(P) (nebo-li comp(P) i= V(->A))
M Úplnost NF pravidla: Nechť P je logický program. Jestliže comp(P) i= V(->A), pak existuje definitivně neúspěšný SLD-strom : -A.
* zůstává problém: není rozhodnutelné, zda daná atomická formule je logickým důsledkem daného logického programu.
M teorém mluví pouze o existenci definitivně neúspěšného SLD-stromu
M definitivně (konečně) neúspěšný SLD-strom sice existuje, ale nemusíme ho nalézt
±  např. v Prologu: může existovat konečné odvození, ale program přesto cyklí (Prolog nenajde definitivně neúspěšný strom)
Hana Rudová, Logické programování I, 14. dubna 2009
9
Negace v logickém programování
Korektnost a úplnost NF pravidla
«• Korektnost NF pravidla: Nechť P logický program a : -A cíl. Jestliže : -A má definitivně neúspěšný SLD-strom, pak V(->A) je logickým důsledkem comp(P) (nebo-li comp(P) i= V(->A))
M Úplnost NF pravidla: Nechť P je logický program. Jestliže comp(P) i= V(->A), pak existuje definitivně neúspěšný SLD-strom : -A.
* zůstává problém: není rozhodnutelné, zda daná atomická formule je logickým důsledkem daného logického programu.
M teorém mluví pouze o existenci definitivně neúspěšného SLD-stromu
M definitivně (konečně) neúspěšný SLD-strom sice existuje, ale nemusíme ho nalézt
±  např. v Prologu: může existovat konečné odvození, ale program přesto cyklí (Prolog nenajde definitivně neúspěšný strom)
-• Odvození pomocí NF pouze test, nelze konstruovat výslednou substituci
-• v(comp(P) i= V(-A)) je A všeob. kvantifikováno, v V(-A) nejsou volné proměnné
Hana Rudová, Logické programování I, 14. dubna 2009
9
Negace v logickém programování
Normální a stratifikované programy
-• normální program: obsahuje negativní literaly v pravidlech -• problém: existence zúplnění, která nemají žádný model
M p : -->p.        zúplnění: p ++ ~^p
M rozdělení programu na vrstvy
M vynucují použití negace relace pouze tehdy pokud je relace úplně definovaná
Hana Rudová, Logické programování I, 14. dubna 2009
10
Negace v logickém programování
Normální a stratifikované programy
-• normální program: obsahuje negativní literaly v pravidlech -• problém: existence zúplnění, která nemají žádný model
M p : -->p.        zúplnění: p ++ ~^p
M rozdělení programu na vrstvy
M vynucují použití negace relace pouze tehdy pokud je relace úplně definovaná
M a.                               a.
a:-^b,a.                 a:-^b,a.
b.                               b : -->a.
Hana Rudová, Logické programování I, 14. dubna 2009
10
Negace v logickém programování
Normální a stratifikované programy
-• normální program: obsahuje negativní literaly v pravidlech -• problém: existence zúplnění, která nemají žádný model
M p : -->p.        zúplnění: p ++ ~^p
M rozdělení programu na vrstvy
M vynucují použití negace relace pouze tehdy pokud je relace úplně definovaná
M a.                               a.
a:-^b,a.                 a:-^b,a.
b.                               b : -->a.
stratifikovaný               není stratifikovaný
Hana Rudová, Logické programování I, 14. dubna 2009
10
Negace v logickém programování
Normální a stratifikované programy
-• normální program: obsahuje negativní literaly v pravidlech -• problém: existence zúplnění, která nemají žádný model
M p : -->p.        zúplnění: p ++ ~^p
M rozdělení programu na vrstvy
M vynucují použití negace relace pouze tehdy pokud je relace úplně definovaná
M a.                               a.
a:-^b,a.                 a:-^b,a.
b.                               b : -->a.
stratifikovaný             není stratifikovaný
-• normální program P je stratifikovaný: množina predikátových symbolů programu lze rozdělit do disjunktních množin So,...,Sm (Si = stratum)
M p(...):-..., q(...),... e P, p e Sk => q £ So u ...u Sk
M p(. ..):-■■■, ~^q{...),...eP,p e Sk ^qE So u...u Sk-i
Hana Rudová, Logické programování I, 14. dubna 2009                      10                                                             Negace v logickém programování
Stratifikované programy II
-• program je m-stratifikovaný <^> m je nejmenší index takový,
že So u ... u Sm je množina všech predikátových symbolů z P
M Věta: Zúplnění každého stratifikovaného programu má Herbrandův model.
3 p : --ip.        nemá Herbrandův model M p : --ip.        ale není stratifikovaný
Hana Rudová, Logické programování I, 14. dubna 2009
1 1
Negace v logickém programování
Stratifikované programy II
-• program je m-stratifikovaný <^> m je nejmenší index takový,
že So u ... u Sm je množina všech predikátových symbolů z P
M Věta: Zúplnění každého stratifikovaného programu má Herbrandův model.
3 p : --ip.        nemá Herbrandův model M p : --ip.        ale není stratifi kovaný
«• stratifikované programy nemusí mít jedinečný minimální Herbrandův model
3 cyklí: -^zastaví.
M dva minimální Herbrandovy modely: {cyklí}, {zastaví}
M důsledek toho, že cyklí: -^zastaví, je ekvivalentní cyklí v zastaví
Hana Rudová, Logické programování I, 14. dubna 2009
1 1
Negace v logickém programování
SLDNF rezoluce: úspěšné odvození
_# NF pravidlo:             :-C. má konečně neúspěšný SLD-strom
-• Pokud máme negativní podcíl ->C v dotazu G, pak hledáme důkaz pro C
M Pokud odvození C selže (strom pro C je konečně neúspěšný), pak je odvození G (i ->C) celkově úspěšné
nahore(X) : - ^blokov any (X). blokovany(X) : -ria(Y,X). na(a,Z?).
Hana Rudová, Logické programování I, 14. dubna 2009
12
Negace v logickém programování
SLDNF rezoluce: úspěšné odvození
NF pravidlo:
- C. má konečně neúspěšný SLD-strom
-• Pokud máme negativní podcíl ->C v dotazu G, pak hledáme důkaz pro C
M Pokud odvození C selže (strom pro C je konečně neúspěšný), pak je odvození G (i ->C) celkově úspěšné
nahore(X) : - ^blokov any (X). blokovany(X) : -ria(Y,X). na(a,Z?).
: -nahore(c) yes
:— nahore(c).
:——i blokovaný(c).
Hana Rudová, Logické programování I, 14. dubna 2009
:- blokovaný(c).
'— na(Y,c).
FAIL
12
úspěšné odvození
Negace v logickém programování
SLDNF rezoluce: neúspěšné odvození
3 NF pravidlo:             :-C. má konečně neúspěšný SLD-strom
-• Pokud máme negativní podcíl ->C v dotazu G, pak hledáme důkaz pro C
-• Pokud existuje vyvrácení C s prázdnou substitucí (strom pro C je konečně úspěšný), pak je odvození G (i ->C) celkově neúspěšné
nahore(X) : - ^blokov any (X). blokovany(X) : -na(Y,X). na(_,_).
Hana Rudová, Logické programování I, 14. dubna 2009
13
Negace v logickém programování
SLDNF rezoluce: neúspěšné odvození
3 NF pravidlo:             :-C. má konečně neúspěšný SLD-strom
-• Pokud máme negativní podcíl ->C v dotazu G, pak hledáme důkaz pro C
-• Pokud existuje vyvrácení C s prázdnou substitucí (strom pro C je konečně úspěšný), pak je odvození G (i ->C) celkově neúspěšné
nahore(X) : - ^blokov any (X). blokovany(X) : -na(Y,X). na(_,_).
: -nahore(X).
no
:- nahore(X).         :- blokovaný(X).
: - -i blokovaný(X).           : - na(Y,X).
^ neúspěšné odvození
Hana Rudová, Logické programování I, 14. dubna 2009                      13                                                             Negace v logickém programování
SLDNF rezoluce: uvázlé odvození
B NF pravidlo:             :-C. má konečně neúspěšný SLD-strom
-• Pokud máme negativní podcíl ->C v dotazu G, pak hledáme důkaz pro C
-• Pokud existuje vyvrácení C s neprázdnou substitucí (strom pro C je konečně úspěšný), pak je odvození G (i ->C) uvázlé
nahore(X) : - ^blokov any (X). blokovany(X) : -na(Y,X). na(a,b).
Hana Rudová, Logické programování I, 14. dubna 2009
14
Negace v logickém programování
SLDNF rezoluce: uvázlé odvození
B NF pravidlo:             :-C. má konečně neúspěšný SLD-strom
-• Pokud máme negativní podcíl ->C v dotazu G, pak hledáme důkaz pro C
-• Pokud existuje vyvrácení C s neprázdnou substitucí (strom pro C je konečně úspěšný), pak je odvození G (i ->C) uvázlé
nahore(X) : - ^blokov any (X). blokovany(X) : -na(Y,X). na(a,b).
: -nahore(X).
:- nahore(X).         :- blokovaný(X).
:——* blokovaný(X).
Hana Rudová, Logické programování I, 14. dubna 2009
:- na(Y,X).
[Y/a,X/b]
=> uvázlé odvození
rxA?i
14                                                             Negace v logickém programování
SLD+ odvození
-• P je normální program, Go normální cíl, R selekční pravidlo: SLD+-odvození Go je buď konečná posloupnost
(Go; Co),..., (Gi-i; Q_i), Gí
nebo nekonečná posloupnost
(Go; Co), (Gi, Ci), (G2; C2),...
kde v každém kroku m + l(m > 0), R vybírá pozitivní literal v Gm a dospívá k Gm+i obvyklým způsobem.
Hana Rudová, Logické programování I, 14. dubna 2009
15
Negace v logickém programování
SLD+ odvození
-• P je normální program, Go normální cíl, R selekční pravidlo: SLD+-odvození Go je buď konečná posloupnost
(Go; Co),..., (Gi-i; Q_i), Gí
nebo nekonečná posloupnost
(Go; Co), (Gi, Ci), (G2; C2),...
kde v každém kroku m + l(m > 0), R vybírá pozitivní literal v Gm a dospívá k Gm+i obvyklým způsobem.
-• konečné SLD+-odvození může být:
1.  úspěšné: Gt = D
2.  neúspěšné
3.  blokované: Gí je negativní (např. ->A)
Hana Rudová, Logické programování I, 14. dubna 2009                      15                                                             Negace v logickém programování
SLDNF rezoluce: pojmy
-• Úroveň cíle
M P normální program, Go normální cíl, R selekční pravidlo: úroveň cíle Go se rovná
± 0 <^> žádné SLD+-odvození s pravidlem R není blokováno * k + 1 <^> maximální úroveň cílů : -A,
které ve tvaru ->A blokují SLD+-odvození Go, je k
3 nekonečná úroveň cíle: blokované SLDNF odvození
Hana Rudová, Logické programování I, 14. dubna 2009
16
Negace v logickém programování
SLDNF rezoluce: pojmy
-• Úroveň cíle
M P normální program, Go normální cíl, R selekční pravidlo: úroveň cíle Go se rovná
± 0 <^> žádné SLD+-odvození s pravidlem R není blokováno * k + 1 <^> maximální úroveň cílů : -A,
které ve tvaru ->A blokují SLD+-odvození Go, je k
3 nekonečná úroveň cíle: blokované SLDNF odvození -• Množina SLDNF odvození = {(SLDNF odvození G0) u (SLDNF odvození: -A)}
3 při odvozování Go jsme se dostali k cíli ->A -• SLDNF odvození cíle G ?
Hana Rudová, Logické programování I, 14. dubna 2009
16
Negace v logickém programování
SLDNF rezoluce
P normální program, Go normální cíl, R selekční pravidlo:
množina SLDNF odvození a podmnožina neúspěšných SLDNF odvození cíle Go
jsou takové nejmenší množiny, že:
-• každé SLD+-odvození Go je SLDNF odvození Go
M je-li SLD+-odvození (Go; Co),..., Gi     blokováno na ->A
3 tj. Gi je tvaru : - Li,... , Lm_i, ->A,Lm+i,... , Ln
pak
Hana Rudová, Logické programování I, 14. dubna 2009
17
Negace v logickém programování
SLDNF rezoluce
P normální program, Go normální cíl, R selekční pravidlo:
množina SLDNF odvození a podmnožina neúspěšných SLDNF odvození cíle Go
jsou takové nejmenší množiny, že:
-• každé SLD+-odvození Go je SLDNF odvození Go
M je-li SLD+-odvození (Go; Co),..., Gi     blokováno na ->A
3 tj. Gi je tvaru : - Li,..., Lm_i, ->A,Lm+i,... ,Ln
pak
3 existuje-li SLDNF odvození: -A (pod R) s prázdnou cílovou substitucí, pak (Go; Co),..., Gi je neúspěšné SLDNF odvození
Hana Rudová, Logické programování I, 14. dubna 2009
17
Negace v logickém programování
SLDNF rezoluce
P normální program, Go normální cíl, R selekční pravidlo:
množina SLDNF odvození a podmnožina neúspěšných SLDNF odvození cíle Go
jsou takové nejmenší množiny, že:
-• každé SLD+-odvození Go je SLDNF odvození Go
M je-li SLD+-odvození (Go; Co),..., Gi     blokováno na ->A
3 tj. Gi je tvaru : - Li,..., Lm_i, ->A,Lm+i,... ,Ln
pak
3 existuje-li SLDNF odvození: -A (pod R) s prázdnou cílovou substitucí, pak (Go; Co),..., Gi je neúspěšné SLDNF odvození
3 je-li každé úplné SLDNF odvození: -A (pod R) neúspěšné pak
\Go; Co), ■ ■ ■ , \Gí, €),('. — Li, ... , Lm_i, Lm+i,. .., Ln) je
(úspěšné) SLDNF odvození cíle Go
±> e označuje prázdnou cílovou substituci
Hana Rudová, Logické programování I, 14. dubna 2009                      17                                                             Negace v logickém programování
SLDNF rezoluce
P normální program, Go normální cíl, R selekční pravidlo:
množina SLDNF odvození a podmnožina neúspěšných SLDNF odvození cíle Go
jsou takové nejmenší množiny, že:
-• každé SLD+-odvození Go je SLDNF odvození Go
M je-li SLD+-odvození (Go; Co),..., Gi     blokováno na ->A
3 tj. Gi je tvaru : - Li,..., Lm_i, ->A,Lm+i,... ,Ln
pak
3 existuje-li SLDNF odvození: -A (pod R) s prázdnou cílovou substitucí, pak (Go; Co),..., Gi je neúspěšné SLDNF odvození
3 je-li každé úplné SLDNF odvození: -A (pod R) neúspěšné pak
\Go; Co), ■ ■ ■ , \Gí, €),('. — Li, ... , Lm_i, Lm+i,. .., Ln) je
(úspěšné) SLDNF odvození cíle Go
±> e označuje prázdnou cílovou substituci
Hana Rudová, Logické programování I, 14. dubna 2009                      17                                                             Negace v logickém programování
Typy SLDNF odvození
Konečné SLDNF-odvození může být:
1. úspěšné: Gi = D
2. neúspěšné
3. uvázlé (flounder):
Gi je negativní (->A) a : -A je úspěšné s neprázdnou cílovou substitucí
4.  blokované: Gi je negativní (->A) a : -A nemá konečnou úroveň.
Hana Rudová, Logické programování I, 14. dubna 2009
18
Negace v logickém programování
Korektnost a úplnost SLDNF odvození
-• korektnost SLDNF-odvození:
P normální program, : -G normální cíl a R je selekční pravidlo: je-li 0 cílová substituce SLDNF-odvození cíle : -G, pak GO je logickým důsledkem comp(P)
Hana Rudová, Logické programování I, 14. dubna 2009
19
Negace v logickém programování
Korektnost a úplnost SLDNF odvození
-• korektnost SLDNF-odvození:
P normální program, : -G normální cíl a R je selekční pravidlo: je-li 0 cílová substituce SLDNF-odvození cíle : -G, pak GO je logickým důsledkem comp(P)
M implementace SLDNF v Prologu není korektní
-• Prolog neřeší uvázlé SLDNF-odvození (neprázdná substituce)
M použití bezpečných cílů (negace neobsahuje proměnné)
Hana Rudová, Logické programování I, 14. dubna 2009
19
Negace v logickém programování
Korektnost a úplnost SLDNF odvození
-• korektnost SLDNF-odvození:
P normální program, : -G normální cíl a R je selekční pravidlo: je-li 0 cílová substituce SLDNF-odvození cíle : -G, pak GO je logickým důsledkem comp(P)
M implementace SLDNF v Prologu není korektní
-• Prolog neřeší uvázlé SLDNF-odvození (neprázdná substituce)
M použití bezpečných cílů (negace neobsahuje proměnné)
-• úplnost SLDNF-odvození: SLDNF-odvození není úplné
-• pokud existuje konečný neúspěšný strom : -A, pak ^A platí
ale místo toho se odvozování: -A může zacyklit, tj. SLDNF rezoluce ^A neodvodí => ^A tedy sice platí, ale SLDNF rezoluce ho nedokáže odvodit
Hana Rudová, Logické programování I, 14. dubna 2009                      19                                                             Negace v logickém programování