Negace v logickém programování
Negativní znalost
& logické programy vyjadřují pozitivní znalost
JS> negativní literály: pozice urCena definicí Hornových klauzulí => nelze vyvodit negativní informaci z logického programu
A každý predikát definuje úplnou relaci
± negativní literál není logickým důsledkem programu
Hana Rudová, Logické programování I, 25. dubna 2012
2
Negace v logickém programování
Negativní znalost
& logické programy vyjadřují pozitivní znalost
JS> negativní literály: pozice urCena definicí Hornových klauzulí => nelze vyvodit negativní informaci z logického programu
A každý predikát definuje úplnou relaci
± negativní literál není logickým dusledkem programu
J5> relace vyjadrený explicitne v nejmenším Herbrandove modelu
S> nad(X,Y) : -na(X, Y). na(c, b).
nad(X, Y) : -na(X, Z),nad(Z, Y). na(b, a).
nejmenší Herbrandův model: {na(b,a),na(c, b),nad(b,a),nad(c, b),nad(c,a)}
Hana Rudová, Logické programování I, 25. dubna 2012
2
Negace v logickém programování
Negativní znalost
& logické programy vyjadřují pozitivní znalost
JS> negativní literály: pozice urCena definicí Hornových klauzulí => nelze vyvodit negativní informaci z logického programu
A každý predikát definuje úplnou relaci
± negativní literál není logickým dusledkem programu
J5> relace vyjadrený explicitne v nejmenším Herbrandove modelu
S> 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)}
& ani program ani model nezahrnují negativní informaci
-i- a není nad c, a není na c
J* i v realite je negativní informace vyjadrena explicitne zrídka, napr. jízdní rád
Hana Rudová, Logické programování I, 25. dubna 2012
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 (closed world assumption, CWA)
převzato z databází
urCitý vztah platí pouze když je vyvoditelný z programu.
P \£ A
„odvozovací pravidlo" (A je (uzavrený) term):-— (CWA)
Hana Rudová, Logické programování I, 25. dubna 2012
3
Negace v logickém programování
Predpoklad uzavřeného sveta
neexistence informace chápána jako opak:
předpoklad uzavřeného sveta (closed world assumption, CWA)
prevzato z databází
urcitý vztah platí pouze když je vyvoditelný z programu.
P \£ A
„odvozovací pravidlo" (A je (uzavrený) term):-— (CWA)
—A
pro SLD-rezoluci: P \£ nad(a,c), tedy lze podle CWA odvodit —nad(a,c)
Hana Rudová, Logické programování I, 25. dubna 2012
3
Negace v logickém programování
Předpoklad uzavřeného světa
C neexistence informace chápána jako opak:
předpoklad uzavřeného sveta (closed world assumption, CWA)
-í* převzato z databází
& urCitý vztah platí pouze když je vyvoditelný z programu.
pro SLD-rezoluci: P £ nad(a,c), tedy lze podle CWA odvodit —nad(a,c)
& problém: není rozhodnutelné, zda daná atomická formule je logickým důsledkem daného logického programu.
-** nelze tedy urát, zda pravidlo CWA je aplikovatelné nebo ne ii> CWA v logickém programování obecne nepoužitelná.
JS> „odvozovací pravidlo" (A je (uzavřený) term):
P £ A
(CWA)
A
Hana Rudová, Logické programování I, 25. dubna 2012
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 (negation as failure, NF)
normální cíl: cíl obsahující i negativní literály
-í* : -nad(c,a), -nad(b,c).
Hana Rudová, Logické programování I, 25. dubna 2012
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á definitívne (koneCne) neúspešný SLD-strom
-A (negation as failure, NF)
M normální cíl: cíl obsahující i negativní literály
-í* : -nad(c,a), -nad(b,c).
-í* rozdíl mezi CWA a NF
-i- program   nad(X,Y) : -nad(X, Y), cíl   : --nad(b,c)
it neexistuje odvození cíle podle NF, protože SLD-strom : -nad(b,c) je nekonecný A existuje odvození cíle podle CWA, protože neexistuje vyvrácení: -nad(b,c)
Hana Rudová, Logické programování I, 25. dubna 2012 4 Negace v logickém programování
Negace jako neúspech (negation as failure)
M slabší verze CWA: definitivně neúspěšný (finitely failed) SLD-strom cíle : -A : -A má definitivně (koneCne) neúspešný SLD-strom
-A (negation as failure, NF)
M normální cíl: cíl obsahující i negativní literály
-í* : -nad(c,a), -nad(b,c).
-í* rozdíl mezi CWA a NF
-i- program   nad(X,Y) : -nad(X, Y), cíl   : --nad(b,c)
neexistuje odvození cíle podle NF, protože SLD-strom : -nad(b,c) je nekoneCný A existuje odvození cíle podle CWA, protože neexistuje vyvrácení: -nad(b,c)
M CWA i NF jsou nekorektní: A není logickým dusledkem programu P
& rešení: definovat programy tak, aby jejich dusledkem byly i negativní literály zúplnění logického programu
Hana Rudová, Logické programování I, 25. dubna 2012 4 Negace v logickém programování
Podstata zúplnění logického programu
prevod všech if príkazu v logickém programu na iff
nad(X,Y) : -na(X,Y).
nad(X, Y) : -na(X, Z),nad(Z,Y).
-i* lze psát jako: nad(X,Y) : -(na(X,Y)) v (na(X, Z),nad(Z,Y)).
zúplnení: nad(X,Y) — (na(X,Y)) v (na(X,Z),nad(Z,Y)).
Hana Rudová, Logické programování I, 25. dubna 2012
5
Negace v logickém programování
Podstata zúplnění logického programu
prevod všech if příkazů v logickém programu na iff
nad(X,Y) : -na(X,Y).
nad(X, Y) : -na(X, Z),nad(Z,Y).
-i* lze psát jako: nad(X,Y) : -(na(X,Y)) v (na(X,Z),nad(Z,Y)).
zúplnení: nad(X,Y)    (na(X,Y)) v (na(X,Z),nad(Z,Y)).
& X je nad Y právě tehdy, když alespoň jedna z podmínek platí
A tedy pokud žádná z podmínek neplatí, X není nad Y
Hana Rudová, Logické programování I, 25. dubna 2012
5
Negace v logickém programování
Podstata zúplnení logického programu
prevod všech if príkazu v logickém programu na iff
nad(X,Y) : -na(X,Y).
nad(X, Y) : -na(X, Z),nad(Z,Y).
-i* lze psát jako: nad(X,Y) : -(na(X,Y)) v (na(X, Z),nad(Z,Y)).
zúplnení: nad(X,Y) — (na(X,Y)) v (na(X,Z),nad(Z,Y)).
& X je nad Y práve tehdy, když alespoň jedna z podmínek platí
A tedy pokud žádná z podmínek neplatí, X není nad Y
kombinace klauzulí je možná pouze pokud mají identické hlavy
S> na(c,b). na(b, a).
S* lze psát jako: na(X\,X2) : -xi = c,X2 = b.
na(X\,X2) : -X1 = b,X2 = a.
-i- zúplnení: na(X1,X2) — (X1 = c,X2 = b) v (X1 = b,X2 = a).
Hana Rudová, Logické programování I, 25. dubna 2012 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: *> comp(P) i= P
s do programuje přidána pouze negativní informace
Hana Rudová, Logické programování I, 25. dubna 2012
6
Negace v logickém programování
Zúplnení přogřamu
Zúplnení přogřamu P je: comp(P) := IFF(P) u CET -í* Základní vlastnosti: *> comp(P) i= P
s do programuje pridána pouze negativní informace
& IFF(P): spojka : - v IF(P) je nahrazena spojkou —
& IF(P): množina všech formulí IF(q,P)
pro všechny predikátové symboly q v programu P
J* Cíl: definovat IF(q,P)
& def(p/n) predikátu p/n je množina všech klauzulí predikátu p/n
Hana Rudová, Logické programování I, 25. dubna 2012
6
Negace v logickém programování
IF(q, P)
na(Xi,X2) : -SY(Xi = c,X2 = b, f (Y)) v (Xi = b,X2 = a, g).
q/n predikátový symbol programu P na(c,b):-f(Y). na(b,a): -g.
X1, ...,Xn jsou „nové" proměnné, které se nevyskytují nikde v P Necht' C je klauzule ve tvaru
kde m > 0, tl,...,tn jsou termy a L1,Lm jsou literály.
Pak označme E(C) výraz 3Y1,Yk(Xl = tl,...,Xn = tn,Ll,... ,Lm) kde Yl,...,Yk jsou všechny promenné v C.
Hana Rudová, Logické programování I, 25. dubna 2012
7
Negace v logickém programování
IF(q, P)
na(Xi,X2) : -SY(Xi = c,X2 = b, f (Y)) v (Xi = b,X2 = a, g).
q/n predikátový symbol programu P na(c,b):-f(Y). na(b,a): -g.
X1, ...,Xn jsou „nové" promenné, které se nevyskytují nikde v P Necht' C je klauzule ve tvaru
q(tl, . . . , tn) : —Ll,..., Lm
kde m > 0, tl,...,tn jsou termy a L1,Lm jsou literály.
Pak oznacme E(C) výraz 3Y1,Yk(Xl = tl,...,Xn = tn,Ll,... ,Lm) kde Yl,...,Yk jsou všechny promenné v C.
Necht' def(q/n) = {C1,Cj}.
Pak formuli IF(q,P) získáme následujícím postupem: q(Xi, ...,Xn) : -E(Ci) v E(C2) v • • • v E(Cj) pro j> 0 a
q(Xl,... ,Xn) : - □ pro j = 0 [q/n není v programu P]
Hana Rudová, Logické programování I, 25. dubna 2012
7
Negace v logickém programování
Clarkova Teorie Rovnosti (CET)
všechny formule jsou univerzálne kvantifikovány:
1. X = X
2. X = Y - Y = X
3. X = Y a Y = Z - X = Z
4. pro každý f/m: Xl = Yl a • • • a Xm = Ym - f(Xl,...,Xm) = f(Yl,...,Ym)
5. pro každý p/m: Xi = Yi a • • • a Xm = Ym - (p(Xi,... ,Xm) - p(Yi,... ,Ym))
6. pro všechny mzné f /m a g/n, (m,n > 0): f(Xi,... ,Xm) = g(Yi,Yn)
7. pro každý f /m: f(Xi ,...,Xm) = f(Yi,...,Ym) - Xi = Yi a • • • a Xm = Ym
8. pro každý term t obsahující X jako vlastní podterm: t = X
X = Y je zkrácený zápis -(X = Y)
Hana Rudová, Logické programování I, 25. dubna 2012
8
Negace v logickém programování
Kořektnost a úplnost NF přavidla
& Kořektnost NF přavidla: Necht' P logický program a : -A cíl. Jestliže : -A má definitívne neúspešný SLD-strom,
pak V (—A) je logickým dusledkem comp(P) (nebo-li comp(P) = V(-A))
Hana Rudová, Logické programování I, 25. dubna 2012
9
Negace v logickém programování
Kořektnost a úplnost NF přavidla
& Kořektnost NF přavidla: Necht' P logický program a : -A cíl. Jestliže : -A má definitivne neúspešný SLD-strom,
pak V (—A) je logickým dusledkem comp(P) (nebo-li comp(P) = V(—A))
JS> Úplnost NF přavidla: Necht' P je logický program. Jestliže comp(P) = V (—A), pak existuje definitivne neúspešný SLD-strom : -A.
-i- zůstává problém: není rozhodnutelné, zda daná atomická formule je logickým důsledkem daného logického programu.
teorém mluví pouze o existenci definitivne neúspešného SLD-stromu
j* definitivne (konecne) neúspešný SLD-strom sice existuje, ale nemusíme ho nalézt
napr. v Prologu: muže existovat konecné odvození, ale program presto cyklí (Prolog nenajde definitivne neúspešný strom)
Hana Rudová, Logické programování I, 25. dubna 2012
9
Negace v logickém programování
Korektnost a úplnost NF pravidla
& Korektnost NF pravidla: Necht' P logický program a : -A cíl. Jestliže : -A má definitívne neúspešný SLD-strom,
pak V (—A) je logickým dusledkem comp(P) (nebo-li comp(P) i= V(-A))
JS> Úplnost NF pravidla: Necht' P je logický program. Jestliže comp(P) = V(-A), pak existuje definitivne neúspešný SLD-strom : -A.
-i- zůstává problém: není rozhodnutelné, zda daná atomická formule je logickým důsledkem daného logického programu.
teorém mluví pouze o existenci definitivne neúspešného SLD-stromu
J* definitivne (konecne) neúspešný SLD-strom sice existuje, ale nemusíme ho nalézt
napr. v Prologu: muže existovat konecné odvození, ale program presto cyklí (Prolog nenajde definitivne neúspešný strom)
Odvození pomocí NF pouze test, nelze konstruovat výslednou substituci
J* v(comp(P) = V(-A))je A všeob. kvantifikováno, v V(-A) nejsou volné promenné
Hana Rudová, Logické programování I, 25. dubna 2012
9
Negace v logickém programování
Normální a stratifikované programy
& normální program: obsahuje negativní literály v pravidlech JS> problém: existence zúplnení, která nemají žádný model p : -—p.      zúplnení: p — —p
M rozdelení programu na vrstvy
j* vynucují použití negace relace pouze tehdy pokud je relace úplne definovaná
Hana Rudová, Logické programování I, 25. dubna 2012
10
Negace v logickém programování
Normální a stratifikované programy
& normální program: obsahuje negativní literály v pravidlech JS> problém: existence zúplnení, která nemají žádný model p : -—p.      zúplnení: p — —p
M rozdelení programu na vrstvy
j* vynucují použití negace relace pouze tehdy pokud je relace úplne definovaná
±> a. a.
a : -—b, a. a : -—b, a.
b. b : -~^a.
Hana Rudová, Logické programování I, 25. dubna 2012 10 Negace v logickém programování
Normální a střatifikované přogřamy
& normální přogřam: obsahuje negativní literály v pravidlech & problém: existence zúplnení, která nemají žádný model
p : -—p.      zúplnení: p — —p
M rozdelení programu na vrstvy
j* vynucují použití negace relace pouze tehdy pokud je relace úplne definovaná
±> a. a.
a : -—b, a. a : -—b, a.
b. b : -—a.
stratifikovaný není stratifikovaný
Hana Rudová, Logické programování I, 25. dubna 2012 10 Negace v logickém programování
Normální a stratifikované programy
& normální program: obsahuje negativní literály v pravidlech JS> problém: existence zúplnení, která nemají žádný model p : -—p.      zúplnení: p -p
M rozdelení programu na vrstvy
& vynucují použití negace relace pouze tehdy pokud je relace úplne definovaná
±> 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 symbolu programu lze rozdelit do disjunktních množin S0,...,Sm (St = stratům)
*> p(...) : -      q(...),... g P, p g Sk => q g So u ... u Sk p(...) : -      —q(...),... g P, p g Sk => q g S0 u ... u Sk-i
Hana Rudová, Logické programování I, 25. dubna 2012 10 Negace v logickém programování
Stratifikované programy II
program je m-stratifikovaný <^> m je nejmenší index takový, že S0 u ... u Sm je množina všech predikátových symbolu z P
& Veta: Zúplnení každého stratifikovaného programu má Herbranduv model.
& p : - — p.      nemá Herbrandův model a p : - — p.      ale není stratifikovaný
Hana R dová, Logické programování I, 25. d bna 2012
11
Negace v logickém programování
Stratifikované programy II
program je m-stratifikovaný <^> m je nejmenší index takový, že S0 u ... u Sm je množina všech predikátových symbolu z P
& Veta: Zúplnení každého stratifikovaného programu má Herbranduv model.
& p : - — p.      nemá Herbrandův model a p : - — p.      ale není stratifikovaný
& stratifikované programy nemusí mít jedinečný minimální Herbrandův model
& cykli: -—zastavi.
s* dva minimální Herbrandovy modely: {cykli}, {zastavi}
M dusledek toho, že cykli: -—zastavi. je ekvivalentní cykli v zastavi
Hana Rudová, Logické programování I, 25. dubna 2012 11 Negace v logickém programování
SLDNF řezoluce: úspešné odvození
C NF pravidlo: : - C. má kone c n e neúsp e šný SLD-strom
—C
£ Pokud máme negativní podcíl —C v dotazu G, pak hledáme dukaz pro C
& Pokud odvození C selže (střom přo C je koneCne neúspešný), pak je odvození G (i —C) celkove úspešné
nahore(X) : - — blokovany(X). blokovany(X) : -na(Y,X). na(a, b).
Hana Rudová, Logické programování I, 25. dubna 2012
12
Negace v logickém programování
C NF pravidlo:
-í* Pokud máme negativní podcíl —C v dotazu G, pak hledáme dukaz pro C
& Pokud odvození C selže (střom přo C je konečně neúspěšný), pak je odvození G (i —C) celkove úspešné
nahore(X) : - — blokovany(X). blokovany(X) : -na(Y,X). na(a, b).
: -nahore(c).
yes
:- nahore(c).
:- blokovany(c).
■
blokovany(c).
■
:- na(Y,c).
FAIL
=> uspešné odvození
Hana Rudová, Logické programování I, 25. dubna 2012
12
Negace v logickém programování
SLDNF rezoluce: neúspešné odvození
C NF pravidlo: : - C. má konecne neúspešný SLD-strom
—C
JS> Pokud máme negativní podcíl —C v dotazu G, pak hledáme dukaz pro C
& Pokud existuje vyvrácení C s prázdnou substitucí (strom pro C je konečne úspešný), pak je odvození G (i — C) celkove neúspešné
nahore(X) :     blokovany(X). blokovany(X) : -na(Y,X). na(_, _).
Hana Rudová, Logické programování I, 25. dubna 2012
13
Negace v logickém programování
JS> NF pravidlo:
Pokud máme negativní podcíl ->C v dotazu G, pak hledáme důkaz pro C
-i* Pokud ěxistujě vyvrácení C s prázdnou substitucí (strom pro C jě koněCně úspěšný), pak jě odvozění G (i — C) cělkově něúspěšné
nahore(X) :     blokov any(X). blokovany(X) : -na(Y,X). na(_, _).
: -nahore(X). no
:- nahore(X).
:- blokovany(X).
■
blokovany(X).
■
:- na(Y,X).
□
=> něúspěšné odvozění
Hana Rudová, Logické programování I, 25. dubna 2012
13
Negace v logickém programování
SLDNF řezoluce: uvázlé odvození
C NF pravidlo: : - C. má konecne neúspešný SLD-strom
—C
JS> Pokud máme negativní podcíl — C v dotazu G, pak hledáme důkaz pro C
£ Pokud existuje vyvřácení C s nepřázdnou substitucí (střom přo C je konecne úspešný), pak je odvození G (i — C) uvázlé
nahore(X) : -—blokovany(X). blokovany(X) : -na(Y,X). na(a, b).
Hana Rudová, Logické programování I, 25. dubna 2012
14
Negace v logickém programování
SLDNF rezoluce: uvázlé odvození
C NF pravidlo: : - C. má konecne neúspešný SLD-strom
——C
JS> Pokud máme negativní podcíl —C v dotazu G, pak hledáme dukaz pro C
£ Pokud existuje vyvrácení C s neprázdnou substitucí (strom pro C je konečne úspešný), pak je odvození G (i —C) uvázlé
nahore(X) : -—blokovany(X). blokovany(X) : -na(Y,X). na(a, b).
: -nahore(X).
:- nahore(X).       :- blokovany(X).
blokovany(X). :- na(Y,X).
| [Y/a,X/b]
^ => uvázlé odvození
[X/b]
Hana Rudová, Logické programování I, 25. dubna 2012 14 Negace v logickém programování
Cvicení: SLDNF odvození
Napište množinu SLDNF odvození pro uvedený dotaz. :- a(B).
a(X) :- b(X), \+ c(X).
a(X) :- d(X), Y is X+1, \+ c(Y), b(X).
b(1).
c(A) :- d(A). d(1).
Hana Rudová, Logické programování I, 25. dubna 2012
15
Negace v logickém programování
SLD+ odvození
P je normální program, G0 normální cíl, R selekcní pravidlo: SLD+-odvození G0 je bud' konecná posloupnost
<Go;Co),..., (Gt-uCt-i),Gt
nebo nekonecná posloupnost
(Go;Co), (Gi;Ci), (G2;C2),...
kde v každém kroku m + l(m > o), R vybírá pozitivní literál v Gm a dospívá k Gm+l obvyklým zpusobem.
Hana Rudová, Logické programování I, 25. dubna 2012
16
Negace v logickém programování
SLD+ odvození
P je normální program, G0 normální cíl, R selekcní pravidlo: SLD+-odvození G0 je bud' konecná posloupnost
(Gól Co),..., (Gi-i, Ci-i), Gi nebo nekonecná posloupnost
(Go, Co), (Gi, Ci), (G2; C2),...
kde v každém kroku m + i(m > 0), R vybírá pozitivní literál v Gm a dospívá k Gm+i obvyklým zpusobem.
muže být:
2. neúspešné
3. blokované: Gi je negativní (napr. -A)
Hana Rudová, Logické programování I, 25. dubna 2012
16
Negace v logickém programování
SLDNF rezoluce: pojmy
& Úroveň cíle
a P normální program, G0 normální cíl, R selekční pravidlo: úroveň cíle G0 se rovná
0 <^> žádné SLD+-odvození s pravidlem R není blokováno Sk + 1 <^> maximální úroven cílů : -A,
které ve tvaru —A blokují SLD+-odvození G0, je k
±> nekonecná úroven
Hana Rudová, Logické programování I, 25. dubna 2012
17
Negace v logickém programování
SLDNF rezoluce: pojmy
Úroven cíle
a P normální program, Go normální cíl, R selekcní pravidlo: úroven cíle Go se rovná
0 <^> žádné SLD+-odvození s pravidlem R není blokováno
M k + 1 <^> maximální úroven cílu : -A,
které ve tvaru —A blokují SLD+-odvození Go, je k
3 nekonecná úroven cíle: blokované SLDNF odvození
Množina SLDNF odvození = {(SLDNF odvození Go) u (SLDNF odvození: -A)} Jr pri odvozování Go jsme se dostali k cíli —A SLDNF odvození cíle G ?
Hana Rudová, Logické programování I, 25. dubna 2012
17
Negace v logickém programování
SLDNF rezoluce
P normální program, G0 normální cíl, R selekcní pravidlo:
množina SLDNF odvození a podmnožina neúspešných SLDNF odvození cíle G0 jsou takové nejmenší množiny, že:
& každé SLD+-odvození G0 je SLDNF odvození G0 & je-li SLD+-odvození (Go; Co>, ...,Gi   blokováno na —A tj. Gi je tvaru : - Li,..., Lm-i, —A, Lm+i,... ,Ln pak
Hana Rudová, Logické programování I, 25. dubna 2012
18
Negace v logickém programování
SLDNF rězolucě
P normální program, G0 normální cíl, R selekcní pravidlo:
množina SLDNF odvozění a podmnožina něúspěšných SLDNF odvozění cíle G0 jsou takové nejmenší množiny, že:
& každé SLD+-odvozění G0 je SLDNF odvození G0 & je-li SLD+-odvození <Go; Co>, ...,Gi   blokováno na —A tj. Gi je tvaru : - Li,..., Lm-i, —A, Lm+i,... ,Ln pak
a ěxistujě-li SLDNF odvozění: -A (pod R) s prázdnou cílovou substitucí, pak <G0; C0>, ...,Gi je něúspěšné SLDNF odvozění
Hana Rudová, Logické programování I, 25. dubna 2012
18
Negace v logickém programování
SLDNF rezoluce
P normální program, G0 normální cíl, R selekcní pravidlo:
množina SLDNF odvození a podmnožina neúspešných SLDNF odvození cíle G0 jsou takové nejmenší množiny, že:
& každé SLD+-odvození G0 je SLDNF odvození G0 & je-li SLD+-odvození (Go; C0), ...,Gi   blokováno na —A tj. Gi je tvaru : - L1,..., Lm-1, —A, Lm+1, ...,Ln pak
a existuje-li SLDNF odvození: -A (pod R) s prázdnou cílovou substitucí, pak (G0; C0), ...,Gi je neúspešné SLDNF odvození
& je-li každé úplné SLDNF odvození: -A (pod R) neúspešné pak
(G0; Co)) . . . ■> (Gii c) j (: - L1 j . . . j Lm-1> Lm+1i . . . , Ln) je
(úspešné) SLDNF odvození cíle G0
c oznacuje prázdnou cílovou substituci
Hana Rudová, Logické programování I, 25. dubna 2012 18 Negace v logickém programování
Typy SLDNF odvození
Konecné SLDNF-odvození může být:
1. úspešné: Gi = □
2. neúspešné
3. uvázlé (flounder):
Gi je negativní (—A) a : -A je úspešné s neprázdnou cílovou substitucí
4. blokované: Gi je negativní (—A) a : -A nemá konecnou úroveň.
Hana Rudová, Logické programování I, 25. dubna 2012
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 9 cílová substituce SLDNF-odvození cíle : -G, pak G9 je logickým dUsledkem comp(P)
Hana Rudová, Logické programování I, 25. dubna 2012
20
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 selekcní pravidlo: je-li 9 cílová substituce SLDNF-odvození cíle : -G, pak G9 je logickým dusledkem comp(P)
s implementace SLDNF v Prologu není korektní
Prolog nereší uvázlé SLDNF-odvození (neprázdná substituce) -i- použití bezpecných cílu (negace neobsahuje promenné)
Hana Rudová, Logické programování I, 25. dubna 2012
20
Negace v logickém programování
Kořektnost a úplnost SLDNF odvození
£ kořektnost SLDNF-odvození:
P normální program, : -G normální cíl a R je selekcní pravidlo: je-li 9 cílová substituce SLDNF-odvození cíle : -G, pak G9 je logickým dusledkem comp(P)
s implementace SLDNF v Prologu není korektní
Prolog nereší uvázlé SLDNF-odvození (neprázdná substituce) -i- použití bezpecných cílu (negace neobsahuje promenné)
úplnost SLDNF-odvození: SLDNF-odvození není úplné
pokud existuje konecný neúspešný strom : -a, pak —A platí ale místo toho se odvozování: -A muže zacyklit, tj. SLDNF rezoluce —A neodvodí == —A tedy sice platí, ale SLDNF rezoluce ho nedokáže odvodit
Hana Rudová, Logické programování I, 25. dubna 2012
20
Negace v logickém programování