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
Hana Rudová, Logické programování I, 6. kvetna 2010
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, 6. kvetna 2010
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, 6. kvetna 2010
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, 6. kvetna 2010
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 (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)
—A
pro SLD-rezoluci: P \£ nad(a, c), tedy lze podle CWA odvodit —nad(a, c)
Hana Rudová, Logické programování I, 6. května 2010
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, 6. kvetna 2010
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ě (koneCne) 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, 6. května 2010
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á definitivne (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)
Hana Rudová, Logické programování I, 6. května 2010 4 Negace v logickém programování
Negace jako neúspěch (negation as failure)
£ slabší verze CWA: definitívne neúspešný (finitely failed) SLD-střom 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)
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úplnení logického přogřamu
Hana Rudová, Logické programování I, 6. kvetna 2010 4 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)).
Hana Rudová, Logické programování I, 6. kvetna 2010
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
Hana Rudová, Logické programování I, 6. kvetna 2010
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
kombinace klauzulí je možná pouze pokud mají identické hlavy
S> na(c,b). na(b, a).
lze psát jako: na(X1,X2) : -X1 = c,X2 = b.
na(X1,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, 6. kvetna 2010 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, 6. května 2010
6
Negace v logickém programování
Zúplnení programu
Zúplnení programu 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, 6. kvetna 2010
6
Negace v logickém programování
IF(4,P)
na(X1,X2) : -3Y(X1 = 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, t1,...,tn jsou termy a L1,Lm jsou literály.
Pak oznaCme E(C) výraz 3Y1,Yk(X1 = t1,...,Xn = tn,L1,... ,Lm) kde Y1,...,Yk jsou všechny promenné v C.
Hana Rudová, Logické programování I, 6. kvetna 2010
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é" proměnné, ktěré sě nevyskytují nikdě v P Něcht' C jě klauzulě vě tvaru
kdě m > 0, tl,...,tn jsou těrmy a L1,Lm jsou litěrály.
Pak oznaCmě E(C) výraz 3Y1,Yk(Xl = tl,...,Xn = tn,Ll,... ,Lm) kdě Yl,...,Yk jsou všěchny proměnné v C.
Něcht' def(q/n) = {C1,Cj}.
Pak formuli IF(q,P) získámě náslědujícím postupěm: q(Xi, ...,Xn) : -E(Ci) v E(C2) v • • • v E(Cj) pro j> 0 a
q(Xl,... ,Xn) : - □ pro j = 0 [q/n nění v programu P]
Hana Rudová, Logické programování I, 6. května 2010
7
Něgacě 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: Xx = Yx 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(Y\,... ,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, 6. kvetna 2010
8
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) £ V(-A))
Hana Rudová, Logické programování I, 6. kvetna 2010
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 dusledkem 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, 6. kvetna 2010
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 dusledkem 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, 6. kvetna 2010
9
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 JS> problém: existence zúplnení, která nemají žádný model a 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, 6. kvetna 2010
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, 6. kvetna 2010
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, 6. kvetna 2010 10 Negace v logickém programování
Normální a stratifikované programy
& normální program: obsahujě něgativní litěrály v pravidlěch & problém: ěxistěncě zúplnění, ktěrá němají žádný moděl
a p : -—p.      zúplnění: p -p
M rozdělění programu na vrstvy
j* vynucují použití něgacě rělacě pouzě těhdy pokud jě rělacě úplně děfinovaná
± a. a.
a : -—b, a. a : -—b, a.
b. b : -—a.
stratifikovaný nění stratifikovaný
& normální program P jě stratifikovaný: množina prědikátových symbolu programu lzě rozdělit do disjunktních množin S0,...,Sm (St = stratům)
*> p(...) : -      q(...), ... g P, p g Sk => q g S0 u ... u Sk p(...) : -      —q(...),... g P, p g Sk => q g S0 u ... u Sk-1
Hana Rudová, Logické programování I, 6. května 2010 10 Něgacě v logickém programování
Střatifikované přogřamy II
program je m-střatifikovaný <^> 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á Herbranduv model a p : --p.      ale není stratifikovaný
Hana Rudová, Logické programování I, 6. kvetna 2010
11
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 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ý
JS> 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, 6. května 2010 11 Negace v logickém programování
SLDNF rězolucě: úspěšné odvození
C NF pravidlo: : - C. má konecne neúspešný SLD-strom
£ Pokud máme negativní podcíl —C v dotazu G, pak hledáme dukaz pro C
& Pokud odvozění C sělžě (strom pro C jě koněCně něúspěšný), pak jě odvozění G (i —C) cělkově úspěšné
nahore(X) : - — blokovany(X). blokovany(X) : -na(Y,X). na(a, b).
Hana Rudová, Logické programování I, 6. kvetna 2010
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, 6. kvetna 2010
12
Negace v logickém programování
SLDNF řezoluce: 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 vyvřácení C s přázdnou substitucí (střom přo C je koneCne ú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, 6. kvetna 2010
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 existuje vyvrácení C s prázdnou substitucí (strom pro C je koneCne úspešný), pak je odvození G (i — C) celkove neúspešné
nahore(X) : - — blokovany(X). blokovany(X) : -na(Y,X). na(_, _).
: -nahore(X). no
:- nahore(X).
:- blokovany(X).
■
blokovany(X).
■
:- na(Y,X).
□
=> neúspešné odvození
Hana Rudová, Logické programování I, 6. kvetna 2010
13
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 důkaz 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).
Hana Rudová, Logické programování I, 6. kvetna 2010
14
Negace v logickém programování
SLDNF rezoluce: uvázlé odvození
C NF pravidlo: : - C. má konecne neúspešný SLD-strom
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 koneCne ú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, 6. kvetna 2010 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í G0 je bud' konečná posloupnost
(Go;Co),..., (Gi-i,Ci-i),Gi
nebo nekonečná posloupnost
(Go, Co), (Gi, Ci), (G2; C2),...
kde v každém kroku m + l(m > o), R vybírá pozitivní literal v Gm a dospívá k Gm+l obvyklým zpusobem.
Hana Rudová, Logické programování I, 6. kvetna 2010
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í G0 je bud' konečná posloupnost
(Go;Co),..., (Gi-iiCi_i>,Gi nebo nekonečná posloupnost
(Go;Co), (Gi;Ci>, (G2;C2>,...
kde v každém kroku m + i (m > o), R vybírá pozitivní literal 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, 6. kvetna 2010
15
Negace v logickém programování
SLDNF rezoluce: pojmy
& Úřoven cíle
a P normální program, G0 normální cíl, R selekcní pravidlo: úřoven cíle G0 se rovná
0 <^> žádné SLD+-odvození s pravidlem R není blokováno 3 k + 1 <^> maximální úroven cílu : -A,
ktěré vě tvaru —A blokují SLD+-odvozění G0, jě k
±> někoněcná úrověn
Hana Rudová, Logické programování I, 6. května 2010
16
Negace v logickém programování
SLDNF řezoluce: pojmy
Úřoven cíle
a P normální program, G0 normální cíl, R selekcní pravidlo: úřoven cíle Go se rovná
0 <^> žádné SLD+-odvození s pravidlem R není blokováno > k + 1 <^> maximální úroven cílu : -A,
které ve tvaru —A blokují SLD+-odvození G0, je k
3 nekonecná úroven cíle: blokované SLDNF odvození
Množina SLDNF odvození = {(SLDNF odvození G0) u (SLDNF odvození: -A)} Jr pri odvozování G0 jsme se dostali k cíli —A SLDNF odvození cíle G ?
Hana Rudová, Logické programování I, 6. kvetna 2010
16
Negace v logickém programování
SLDNF řezoluce
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, 6. kvetna 2010
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
a existuje-li SLDNF odvození: -A (pod R) s prázdnou cílovou substitucí, pak (G0; C0>, ...,Gi je neúspešné SLDNF odvození
Hana Rudová, Logické programování I, 6. kvetna 2010
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 : - L\,..., Lm-i, —A, Lm+\,... ,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; C0>) . . . ■> (Gii £>j(: - L1 j . . . j Lm-1) Lm+1) . . . ■> Ln) je
(úspešné) SLDNF odvození cíle g0
e oznacuje prázdnou cílovou substituci
Hana Rudová, Logické programování I, 6. kvetna 2010 17 Negace v logickém programování
Typy SLDNF odvozění
Konecné SLDNF-odvození může být:
1. úspěšné: Gi = □
2. něúspěšné
3. uvázlé (flounder):
Gi je negativní (—A) a : -A je úspešné s něprázdnou cílovou substitucí
4. blokované: Gi je negativní (—A) a : -A nemá konecnou úroven.
Hana Rudová, Logické programování I, 6. kvetna 2010
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 9 cílová substituce SLDNF-odvození cíle : -G, pak G9 je logickým důsledkem comp(P)
Hana Rudová, Logické programování I, 6. kvetna 2010
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 jě sělěkcní pravidlo: jě-li 9 cílová substitucě SLDNF-odvozění cílě : -G, pak G9 jě logickým důslědkěm comp(P)
s implěměntacě SLDNF v Prologu nění korěktní
Prolog něrěší uvázlé SLDNF-odvozění (něprázdná substitucě) -i- použití bězpěcných cílu (něgacě něobsahujě proměnné)
Hana Rudová, Logické programování I, 6. května 2010
19
Něgacě 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)
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, 6. kvetna 2010
19
Negace v logickém programování