Negace v logickém programování
Negativní znalost
logické programy vyjadřují pozitivní znalost
negativní literály: pozice určena definicí Hornových klauzulí => nelze vyvodit negativní informaci z logického programu
■ každý predikát definuje úplnou relaci
■ negativní literál není logickým důsledkem programu
relace vyjádřeny explicitně v nejmenším Herbrandově modelu
' nad(X,Y) :-na(X,Y). na(c,b). nad(X, Y) : -na(X, Z),nad(Z, Y). na(b, a).
■ nej menší Herbrandúv model: {na(b, a),na(c, b),nad(b, a),nad(c,b),nad(c, a)} ani program ani model nezahrnují negativní informaci
■ a není nad c, a není na c
■ i v realitě je negativní informace vyjádřena explicitně zřídka, např. jízdní řád
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 if A
„odvozovací pravidlo" (A je (uzavřený) term):
->A
(CWA)
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čit, zda pravidlo CWAje aplikovatelné nebo ne CWA v logickém programování obecně nepoužitelná.
Hana Rudová, Logické programování I, 6. května 2010
Negace v logickém programování
Hana Rudová, Logické programování I, 6. května 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ě (konečně) neúspěšný SLD-strom
(negation as failure, IMF
normální cíl: cíl obsahující i negativní literály
■ : -nad(c,a), -inad(b,c). rozdíl mezi CWA a NF
■program   nad(X,Y) : -nad(X,Y), cíl :--inad(b,c)
■ 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, 6. května 2010
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
■ nad(X,Y) : -na(X,Y).
nad(X, Y) : -na(X,Z),nad(Z, Y). * lze psát jako: nad(X,Y) : -(na(X,Y)) v (na(X,Z),nad(Z,Y)).
■ zúplnění: 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í
■ tedy pokud žádná z podmínek neplatí, X není nad Y kombinace klauzulí je možná pouze pokud mají identické hlavy
■ na(c,b). na(b, a).
■ lze psát jako: na(Xi,X2) '■ —X\ = c,X2 = b.
na(XuX2) : -Xi = b,X2 = a.
■ zúplnění: na(Xi,X2) « (Xi = c,X2 = b)v (Xi = b,X2 = a).
Hana Rudová, Logické programování I, 6. května 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
■ do programuje přidá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
■ Cíl: definovat l¥(q,P)
■ de f (pln) predikátu p In je množina všech klauzulí predikátu pln
Hana Rudová, Logické programování I, 6. května 201 0 6 Negace v logickém programován
na(XuX2) : -3Y(Xi = c,X2 = bJ(Y)) v (Xi = 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(h, ■ ■ ■, tn) : -Li,... ,Lm
kde m > 0, t\,..., tn jsou termy a Li,... ,Lm jsou literály.
Pak označme E(C) výraz 3Yi,Yu(X\ = t\,... ,Xn = tn,L\,... ,Lm) kde Y\,..., ľk jsou všechny proměnné v C.
Nechť de f (q In) = {Ci,..., C,}.
Pak formuli l¥(q,P) získáme následujícím postupem:
q(X1,...,Xn) : -E(Ci) VE(C2) v ■ ■ ■ v E(C,) pro j > 0a
q(X\,... ,Xn) '■ - □ pro j = 0 [q/n není v programu P
Hana Rudová, Logické programování I, 6. května 2010 7 Negace v logickém programování
Clarkova Teorie Rovnosti (CET)
všechny formule jsou univerzálně kvantifikovány:
1. X = X
2. X=Y^Y = X
3. X=YaY = Z^X = Z
4. pro každý f/m: Xi = Yx A ■ ■ ■ A Xm = Ym - f(Xu ..., Xm) = f(Ylt..., Ym)
5. pro každý p/m: Xx = Yx A ■ ■ ■ A Xm = Ym - (p(Xlt...,Xm) - p(Ylt..., Ym))
6. pro všechny různé f/m. a g/n, (m, n > 0): f(X\,... ,Xm) ± g(Y\,..., Yn)
7. pro každý f/m: f(X1,...,Xm) = f(Y1,...,Ym) —► X\ = Y\ /\ ■ ■ ■ /\ Xm = Ym
8. pro každý term ř obsahující X jako vlastní podterm: ř ^ X
X ± Y je zkrácený zápis -<(X = Y)
Hana Rudová, Logické programování I, 6. května 201 0 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(-iA) je logickým důsledkem comp(P) (nebo-li comp(P) i= V(-iA))
Úplnost NF pravidla: Nechť P je logický program. Jestliže comp(P) i= V(-iA), 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.
■ teorém mluví pouze o existenci definitivně neúspěšného SLD-stromu
■ 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(-vl)) je A všeob. kvantifikováno, v V(-vl) nejsou volné proměnné
Hana Rudová, Logické programování I, 6. května 2010
Negace v logickém programování
St ratifikované 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
Věta: Zúplnění každého stratifikovaného programu má Herbrandův model.
■ p :-~<p.      nemá Herbrandův model
■ p : -~<p.      ale není stratifikovaný
stratifikované programy nemusí mít jedinečný minimální Herbrandův model
■ cyklí: -^zastaví.
■ dva minimální Herbrandovy modely: {cyklí}, {zastaví}
■ důsledek toho, že cyklí: -^zastaví, je ekvivalentní cyklí v zastaví
Hana Rudová, Logické programování I, 6. května 2010
Negace v logickém programování
Normální a stratifikované programy
normální program: obsahuje negativní literály v pravidlech problém: existence zúplnění, která nemají žádný model
■ p : -->p. zúplnění: p «- -ip rozdělení programu na vrstvy
■ vynucují použití negace relace pouze tehdy pokud je relace úplně definovaná
a.
a: --li?, a.
b.
a.
a: --ifc, a. b : --ifl.
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 = stratům)
■ p(...):-..., q(...),... e P, p e Sk => q e S0 u ... u Sk
■ p(...):-..., -.<?(...),... e P, p e Sk => q e S0 u ... u Sk-i
Hana Rudová, Logické programování I, 6. května 2010
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
■ 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) : -^blokovaný(X). blokovaný(X) : -na(Y,X). na(a, b).
: -nahore(c).
yes :— nahore(c).
blokovany(c).
blokovaný (c). I
:— na(Y,c). I
FAIL
úspěšné odvození
Hana Rudová, Logické programování I, 6. května 2010
Negace v logickém programován
SLDNF rezoluce: neú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
■ 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) : -^blokovaný(X). blokovaný(X) : -na(Y,X). na(_, _).
: -nahore(X).
:- nahore(X).        •'- blokovany(X).
| I
blokovany(X). •'- na(Y,X).
I
O => neúspěšné odvození
Hana Rudová, Logické programování I, 6. května 2010 13 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),..., (Gj-i; Cí-i), Gi
nebo nekonečná posloupnost
<G0;C0>,<Gi;Ci>,<G2;C2>,...
kde v každém kroku m + l(m > 0), R vybírá pozitivní literál v Gm a dospívá k Gm+\ obvyklým způsobem.
■ konečné SLD+-odvození může být:
1. úspěšné: Gi = □
2. neúspěšné
3. blokované: Gi je negativní (např. -^A)
Hana Rudová, Logické programování I, 6. května 2010 1 5 Negace v logickém programování
SLDNF rezoluce: uvázlé 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
■ 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) : -^blokovaný(X). blokovaný(X) : -na(Y,X). na(a, b).
■-nahore(X).      ._ nahore(X).       :-blokovaný(X).
I I
blokovany(X). •'- na(Y,X).
| [Y/a,X/b] □
[X/b] => uvázlé odvození
Hana Rudová, Logické programování I, 6. května 201 0 1 4 Negace v logickém programování
SLDNF rezoluce: pojmy
■ Úroveň cíle
■ 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
■ nekonečná úroveň cíle: blokované SLDNF odvození
■ Množina SLDNF odvození = {(SLDNF odvození G0) u (SLDNF odvození : -A)}
■ při odvozování Go jsme se dostali k cíli -<A
■ SLDNF odvození cíle G ?
Hana Rudová, Logické programování I, 6. května 201 0 1 6 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
■ je-li SLD+-odvození (Go; Co),..., Gi   blokováno na -<A
* tj. Grje tvaru : - Lu ... ,Lm-i, -^A,Lm+1,... ,Ln pak
■ existuje-li SLDNF odvození: -A (pod R) s prázdnou cílovou substitucí, pak (Go; Co),..., Gi je neúspěšné SLDNF odvození
■ je-li každé úplné SLDNF odvození: -A (pod R) neúspěšné pak
(Go; Co>,..., (Gi, e>,(: — 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í 1,6. května 2010 17 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)
■ implementace SLDNF v Prologu není korektní
■ Prolog neřeší uvázlé SLDNF-odvození (neprázdná substituce)
■ 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 -iA platí
ale místo toho se odvozování: -A může zacyklit, tj. SLDNF rezoluce -iA neodvodí => -iA tedy sice platí, ale SLDNF rezoluce ho nedokáže odvodit
Typy SLDNF odvození
Konečné SLDNF-odvození může být:
1. úspěšné: Gi = □
2. neúspěšné
3. uvázlé (flounder):
Gj 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, 6. května 2010
Negace v logickém programování
Hana Rudová, Logické programování 1,6. května 2010 19 Negace v logickém programování