Operační a deklarativní sémantika
Operační sémantika
JS> Operační sémantikou logického programu P rozumíme množinu O(P) všech atomických formulí bez proměnných, které lze pro nejaký cíl g1 odvodit nejakým rezolucním dukazem ze vstupní množiny P u {g}.
1tímto výrazem jsou míneny všechny cíle, pro než zmínený rezolucní dukaz existuje.
Hana Rudová, Logické programování I, 9. dubna 2013
2
Sémantiky
Operační sémantika
JS> Operační sémantikou logického programu P rozumíme množinu O(P) všech atomických formulí bez proměnných, které lze pro nejaký cíl g1 odvodit nejakým rezolucním důkazem ze vstupní množiny P u {g}.
1tímto výrazem jsou míneny všechny cíle, pro než zmínený rezolucní dukaz existuje.
& Deklarativní sémantika logického programu P ???
Hana Rudová, Logické programování I, 9. dubna 2013
2
Sémantiky
Opakování: interpretace
& Interpretace I jazyka L je dána univerzem D a zobrazením, které přiřadí konstantě c prvek D, funkčnímu symbolu f/n n-ární operaci v D a predikátovému symbolu p/n n-ární relaci.
príklad: F = {{f(a,b) = f (b,a)}, {f(f(a,a),b) = a}} interpretace ?i: D = Z, a := 1,b := -1,f := " + "
Hana Rudová, Logické programování I, 9. dubna 2013
3
Sémantiky
Opakování: interpretace
& Interpretace I jazyka L je dána univerzem D a zobrazením, které přiřadí konstantě c prvek D, funkčnímu symbolu f/n n-ární operaci v D a predikátovému symbolu p/n n-ární relaci.
príklad: F = {{f(a,b) = f (b,a)}, {f(f(a,a),b) = a}} interpretace 11: D = Z, a := 1,b := -1,f := " + "
Interpretace se nazývá modelem formule, je-li v ní tato formule pravdivá interpretace množiny N s obvyklými operacemi je modelem formule ( 0 + s(0) = s(0))
Hana Rudová, Logické programování I, 9. dubna 2013
3
Sémantiky
Herbrandovy interpretace
& Omezení na obor skládající se ze symbolických výrazů tvorených z predikátových a fůnkCních symbolů daného jazyka
i* pri zkoumání pravdivosti není nutné uvažovat modely nad všemi interpretacemi
Hana Rudová, Logické programování I, 9. dubna 2013
4
Sémantiky
Herbrandovy interpretace
Omezení na obor skládající se ze symbolických výrazů tvorených z predikátových a fůnkCních symbolů daného jazyka
i* pri zkoumání pravdivosti není nutné uvažovat modely nad všemi interpretacemi
Herbrandovo univerzům: množina všech termU bez proměnných, které mohou být tvořeny funkcními symboly a konstantami daného jazyka
Herbrandova interpretace: libovolná interpretace, která prirazuje
i* promenným prvky Herbrandova univerza Jť konstantám sebe samé
j* funkcním symbolum funkce, které symbolu f pro argumenty t1, • • • ,tn priradí term
f(tl, • • • ,tn)
J* predikátovým symbolum libovolnou funkci z Herbrand. univerza do pravdivostních hodnot
Hana Rudová, Logické programování I, 9. dubna 2013
4
Sémantiky
Herbrandovy interpretace
& Omezení na obor skládající se ze symbolických výrazů tvorených z predikátových a fůnkCních symbolů daného jazyka
i* pri zkoumání pravdivosti není nutné uvažovat modely nad všemi interpretacemi
JS> Herbrandovo univerzům: množina všech termU bez proměnných, které mohou být tvořeny funkcními symboly a konstantami daného jazyka
i* promenným prvky Herbrandova univerza Jť konstantám sebe samé
j* funkcním symboium funkce, které symbolu f pro argumenty t1, • • • ,tn priradí term
f(tl, • • • ,tn)
J* predikátovým symbolum libovolnou funkci z Herbrand. univerza do pravdivostních hodnot
& Herbrandův model množiny uzavrených formulí P:
Herbrandova interpretace taková, že každá formule z P je v ní pravdivá.
prirazuje
Hana Rudová, Logické programování I, 9. dubna 2013
4
Sémantiky
Specifikace Herbrandova modelu
C Herbrandovy interpretace mají předdefinovaný význam funktorů a konstant
-í* Pro specifikaci Herbrandovy interpretace tedy staCí zadat relace pro každý predikátový symbol
Hana Rudová, Logické programování I, 9. dubna 2013
5
Sémantiky
Specifikace Herbrandova modelu
C Herbrandovy interpretace mají předdefinovaný význam funktorů a konstant
-í* Pro specifikaci Herbrandovy interpretace tedy staCí zadat relace pro každý predikátový symbol
& Príklad: Herbrandova interpretace a Herbrandův model množiny formulí
1ichy(s(0)). % (1)
1ichy(s(s(X))) :- lichy(X). % (2)
Hana Rudová, Logické programování I, 9. dubna 2013
5
Sémantiky
Specifikace Herbrandova modelu
C Herbrandovy interpretace mají preddefinovaný význam funktom a konstant
& Pro specifikaci Herbrandovy interpretace tedy stací zadat relace pro každý predikátový symbol
& Príklad: Herbrandova interpretace a Herbranduv model množiny formulí
1ichy(s(0)). % (1)
1ichy(s(s(X))) :- lichy(X). % (2)
a I1 = 0 není model (1)
Hana Rudová, Logické programování I, 9. dubna 2013
5
Sémantiky
Specifikace Herbrandova modelu
C Herbrandovy interpretace mají předdefinovaný význam funktorů a konstant
-í* Pro specifikaci Herbrandovy interpretace tedy staCí zadat relace pro každý predikátový symbol
& Príklad: Herbrandova interpretace a Herbrandův model množiny formulí
1ichy(s(0)). % (1)
1ichy(s(s(X))) :- lichy(X). % (2)
a I1 = 0 není model (1)
a 12 = {lichy(s(0))} není model (2)
Hana Rudová, Logické programování I, 9. dubna 2013
5
Sémantiky
Specifikace Herbrandova modelu
C Herbrandovy interpretace mají preddefinovaný význam funktorů a konstant
ü> Pro specifikaci Herbrandovy interpretace tedy staCí zadat relace pro každý predikátový symbol
& Príklad: Herbrandova interpretace a Herbrandův model množiny formulí
1ichy(s(0)). % (1)
1ichy(s(s(X))) :- lichy(X). % (2)
a I1 = 0 není model (1)
a 12 = {lichy(s(0))} není model (2)
I3 = {lichy (s(0)), lichy(s(s(s(0))))} není model (2)
Hana Rudová, Logické programování I, 9. dubna 2013
5
Sémantiky
Specifikace Herbrandova modelu
C Herbrandovy interpretace mají předdefinovaný význam funktorů a konstant
-í* Pro specifikaci Herbrandovy interpretace tedy staCí zadat relace pro každý predikátový symbol
& Príklad: Herbrandova interpretace a Herbrandův model množiny formulí
1ichy(s(0)). % (1)
1ichy(s(s(X))) :- lichy(X). % (2)
a I1 = 0 není model (1)
a 12 = {lichy (s(0))} není model (2)
13 = {lichy (s(0)), lichy(s(s(s(0))))} není model (2)
14 = {lichy (sn(0))\n e {1, 3, 5, 7,...}} Herbrandův model (1) i (2)
Hana Rudová, Logické programování I, 9. dubna 2013
5
Sémantiky
Specifikace Herbrandova modelu
Herbrandovy interpretace mají předdefinovaný význam funktorů a konstant
Pro specifikaci Herbrandovy interpretace tedy staCí zadat relace pro každý predikátový symbol
Príklad: Herbrandova interpretace a Herbrandův model množiny formulí
1ichy(s(0)). % (1)
1ichy(s(s(X))) :- lichy(X). % (2)
a I1 = 0 není model (1)
a 12 = {lichy (s(0))} není model (2)
13 = {lichy (s(0)), lichy(s(s(s(0))))} není model (2)
14 = {lichy (sn(0))\n e {1, 3, 5, 7,...}} Herbrandův model (1) i (2)
15 = {lichy(sn(0))\n e N}} Herbrandův model (1) i (2)
Hana Rudová, Logické programování I, 9. dubna 2013
5
Sémantiky
Príklad: Herbrandovy interpretace
rodic(a,b). rodic(b,c). predek(X,Y) predek(X,Z)
rodic(X,Y). rodic(X,Y),
predek(Y,Z).
Hana Rudová, Logické programování I, 9. dubna 2013
6
Sémantiky
Príklad: Herbrandovy interpretace
rodic(a,b). rodic(b,c).
predek(X,Y) :- rodic(X,Y).
predek(X,Z) :- rodic(X,Y), predek(Y,Z).
11 = {rodic(a, b),rodic(b, c),predek(a, b),predek(b, c),predek(a, c)}
12 = {rodic(a,b),rodic(b,c),
predek(a, b), predek(b, c), predek(a, c), predek(a, a)}
11 i 12 jsou Herbrandovy modely klauzulí
Cvicení: Napište minimální Herbranduv model pro následující logický program.
muz(petr). muz(pavel). zena(olga). zena(jitka). pary(X,Y) :- zena(X), muz(Y).
Uved'te další model tohoto programu, který není minimální.
Hana Rudová, Logické programování I, 9. dubna 2013 6 Sémantiky
a operacní sémantika
ii> Je-li S množina programových klauzulí a M libovolná množina Herbrandových modelu S, pak průnik techto modelů je opet Herbranduv model množiny S.
JS> Důsledek:
Existuje nejmenší Herbrandův model množiny S, který znacíme M(S).
Hana Rudová, Logické programování I, 9. dubna 2013
7
Sémantiky
a operacní sémantika
ii> Je-li S množina programových klauzulí a M libovolná množina Herbrandových modelu S, pak průnik techto modelů je opet Herbrandův model množiny S.
JS> Důsledek:
Existuje nejmenší Herbrandův model množiny S, který znacíme M(S).
-á* Deklarativní sémantikoů logického programu P rozumíme jeho minimální Herbrandův model M(P).
Hana Rudová, Logické programování I, 9. dubna 2013
7
Sémantiky
a operaCní sémantika
ii> Je-li S množina programových klauzulí a M libovolná množina Herbrandových modelu S, pak průnik techto modelů je opet Herbrandův model množiny S.
JS> Důsledek:
Existuje nejmenší Herbrandův model množiny S, který znacíme M(S).
-á* Deklarativní sémantikou logického programu P rozumíme jeho minimální Herbrandův model M(P).
& Pripomenutí: Operacní sémantikou logického programu P rozumíme
množinu O(P) všech atomických formulí bez promenných, které lze pro nejaký cíl Q1 odvodit nejakým rezolucním dukazem ze vstupní množiny P u {Q}.
1tímto výrazem jsou míneny všechny cíle, pro než zmínený rezolucní dukaz existuje.
Hana Rudová, Logické programování I, 9. dubna 2013
7
Sémantiky
a operacní sémantika
ii> Je-li S množina programovýCh klauzulí a M libovolná množina HerbrandovýCh modelu S, pak průnik techto modelů je opet Herbrandův model množiny S.
JS> Důsledek:
Existuje nejmenší Herbrandův model množiny S, který znaCíme M(S).
-á* Deklarativní sémantikou logiCkého programu P rozumíme jeho minimální Herbrandův model M(P).
& Pripomenutí: Operacní sémantikou logiCkého programu P rozumíme
množinu O(P) všeCh atomiCkýCh formulí bez promennýCh, které lze pro nejaký Cíl Q1 odvodit nejakým rezoluCním dukazem ze vstupní množiny P u {Q}.
Hímto výrazem jsou míneny všeChny Cíle, pro než zmínený rezoluCní dukaz existuje.
-i* Pro libovolný logiCký program P platí      M(P) = O(P)
Hana Rudová, LogiCké programování I, 9. dubna 2013
7
Sémantiky
SLD rezoluce v Prologu (pokraCování)
Výpocetní strategie
Korektní výpocetní strategie prohledávání stromu výpoCtu musí zaruCit, že se každý (koneCný) výsledek nalézt v koneCném Case
Hana Rudová, Logické programování I, 9. dubna 2013
9
SLD rezoluCe v Prologu
Výpocetní strategie
Korektní výpocetní strategie prohledávání stromu výpoctu musí zarucit, že se každý (konecný) výsledek nalézt v konecném case
& Korektní výpocetní strategie = prohledávání stromů do šírky
& exponenciální pamet'ová nárocnost a složité rídící struktury
Hana Rudová, Logické programování I, 9. dubna 2013
9
SLD rezoluce v Prologu
Výpočetní strategie
Korektní výpočetní strategie prohledávání stromu výpoctu musí zarucit, že se každý (konecný) výsledek nalézt v konecném case
& Korektní výpocetní strategie = prohledávání stromu do šírky
& exponenciální pamet'ová nárocnost a složité rídící struktury
JS> Použitelná výpocetní strategie = prohledávání stromu do hloubky
& jednoduché rídící struktury (zásobník) * lineární pamet'ová nárocnost
s> není ale úplná: nenalezne vyvrácení i když existuje
procházení nekonecné vetve stromu výpoctu => na nekonecných stromech dojde k zacyklení nedostaneme se tak na jiné existující úspešné uzly
Hana Rudová, Logické programování I, 9. dubna 2013 9 SLD rezoluce v Prologu
SLD-rezolůce v Prologů: úplnost
-í* Prolog: prohledávání stromu do hloubky
=> neúplnost použité výpocetní strategie
-i* Implementace SLD-rezoluce v Prologu
a není úplná
logický program: q : -r. (1)
r : -q. (2)
q. (3) dotaz: : -q.
:- q.
:- r. □
Hana Rudová, Logické programování I, 9. dubna 2013
10
SLD rezoluce v Prologu
Test výskytu
Kontrola, zda se promenná vyskytuje v termu, kterým ji substituujeme
A dotaz : -a(B,B). i> logický program: a(X,f(X)). by vedl k: [B/X], [X/f(X)]
Unifikátor pro g(Xi, ...,Xn) a g(f(Xo,Xo),f(Xl,Xl),... ,f(Xn-i,Xn-i))
Xi = f(Xo,Xo),   X2 = f(Xi,Xi),...,    Xn = f(Xn-l,Xn-l)
X2 = f(f(Xo,Xo),f(Xo,Xo)),... délka termu pro Xk exponenciálne narůstá
Hana Rudová, Logické programování I, 9. dubna 2013
11
SLD rezoluce v Prologu
Test výskytu
-í* Kontrola, zda se promenná vyskytuje v termu, kterým ji substituujeme
A dotaz : -a(B,B). i> logický program: a(X,f(X)). by vedl k: [B/X], [X/f(X)]
& Unifikátor pro g(Xi, ...,Xn) a g(f(Xo,Xo),f(Xi,Xi),.. .,f(Xn-i,Xn-i))
Xi = f(Xo,Xo),   X2 = f(Xi,Xi),...,    Xn = f(Xn-l,Xn-l)
X2 = f(f(Xo,Xo),f(Xo,Xo)),...
délka termu pro Xk exponenciálne narůstá => exponenciální složitost na overení kontroly výskytu JS> Test výskytu se pri unifikaci v Prologu neprovádí
* Dusledek:      ? - X = f(X) uspeje s X = f (f (f (f (f (f (f (f (f (f (...))))))))))
Hana Řudová, Logické programování I, 9. dubna 2013 11 SLD rezoluce v Prologu
SLD-rezoluče v Prologu: korektnost
-í* Implementace SLD-rezoluce v Prologu nepoužívá pri unifikaci test výskytu
=> není korektní
(1) t(X) : -p(X,X).    : -t(X).
p(X,f(X)). X = f (f(f(f (...))))))))))      problém se projeví
Hana Rudová, Logické programování I, 9. dubna 2013
12
SLD rezoluce v Prologu
SLD-rezoluce v Prologu: korektnost
-í* Implementace SLD-rezoluce v Prologu nepoužívá pri unifikaci test výskytu => není korektní
(1) t(X) : -p(X,X).    : -t(X).
p(X,f(X)). X = f (f(f(f (...))))))))))      problém se projeví
(2) t : -p(X,X).        : -t.
p(X,f(X)). yes      dokazovací systém nehledá unifikátor pro X a f(X)
Hana Rudová, Logické programování I, 9. dubna 2013
12
SLD rezoluce v Prologu
SLD-rezolůce v Prologů: korektnost
-í* Implementace SLD-rezoluce v Prologu nepoužívá pri unifikaci test výskytu => není korektní
(1) t(X) : -p(X,X).    : -t(X).
p(X,f(X)). X = f (f(f(f (...))))))))))      problém se projeví
(2) t : -p(X,X).        : -t.
p(X,f(X)). yes      dokazovací systém nehledá unifikátor pro X a f(X)
-í* Rešení: problém typu (2) prevést na problém typu (1) ?
Hana Rudová, Logické programování I, 9. dubna 2013
12
SLD rezoluce v Prologu
SLD-rezoluce v Prologu: korektnost
Implementace SLD-rezoluce v Prologu nepoužívá při unifikaci test výskytu
není korektní
(1) t(X) : -p(X,X).    : -t(X).
p(X,f(X)). X = f (f(f(f (...))))))))))      problém se projeví
(2) t : -p(X,X) p(X,f(X)).
: -t. yes
dokazovací systém nehledá unifikátor pro X a f(X)
Řešení: problém typu (2) převést na problém typu (1) ?
*> každá promenná v hlave klauzule se objeví i v tele, aby se vynutilo hledání unifikátoru (pridáme X = X pro každou X, která se vyskytuje pouze v hlave)
t: -p(X,X). p(X,f(X)) : -X = X.
Hana Řudová, Logické programování I, 9. dubna 2013
12
SLD rezoluce v Prologu
SLD-rezoluce v Prologu: korektnost
Implementace SLD-rezoluce v Prologu nepoužívá při unifikaci test výskytu
není korektní
(1) t(X) : -p(X,X).    : -t(X).
p(X,f(X)). X = f (f(f(f (...))))))))))      problém se projeví
(2) t : -p(X,X) p(X,f(X)).
: -t. yes
dokazovací systém nehledá unifikátor pro X a f(X)
Řešení: problém typu (2) převést na problém typu (1) ?
*> každá promenná v hlave klauzule se objeví i v tele, aby se vynutilo hledání unifikátoru (pridáme X = X pro každou X, která se vyskytuje pouze v hlave)
t: -p(X,X). p(X,f(X)) : -X = X.
a optimalizace v kompilátoru mohou způsobit opet odpoved' „yes"
Hana Řudová, Logické programování I, 9. dubna 2013
12
SLD rezoluce v Prologu
Řízení implementace:
JS> rez se syntakticky chová jako kterýkoliv jiný literál
& nemá ale žádnou deklarativní sémantiku
JS> místo toho mení implementaci programu
*> p : -q, !,v.
ořezání
Hana Rudová, Logické programování I, 9. dubna 2013
13
SLD rezoluce v Prologu
Řízení implementace: rez
rez se syntakticky chová jako kterýkoliv jiný literál nemá ale žádnou deklarativní sémantiku místo toho mení implementaci programu
p : -q, !,v. snažíme se splnit q
pokud uspeji
=> preskocím rez a pokracuji jako by tam rez nebyl
:- q,!,v.
upnutí
ořezání
pokud ale neuspěji (a tedy i pri backtrackingu) a vracím se pres rez => vracím se až na rodice : -p. a zkouším další vetev
Hana Rudová, Logické programování I, 9. dubna 2013
13
SLD rezoluce v Prologu
Řízení implementace: rez
r ez se syntakticky chová jako kterýkoliv jiný literál nemá ale žádnou deklarativní sémantiku místo toho mení implementaci programu
p : -q, !,v. snažíme se splnit q
pokud uspeji
=> p reskocím rez a pokracuji jako by tam r ez nebyl
:- q,!,v.
upnutí
ořezání
pokud ale neuspeji (a tedy i pri bačktračkingu) a vračím se pres rez => vračím se až na rodiče : -p. a zkouším další vetev => nezkouším tedy další možnosti, jak splnit p upnutí => a nezkouším ani další možnosti, jak splnit q v SLD-stromu        o r ezání
Hana Rudová, Logické programování I, 9. dubna 2013
13
SLD rezoluce v Prologu
Příklad: řez
t: -p,r. t: -s.
p : -q(X), \,v,
p : -u,w.
q(a).
q(b).
s.
u.
(1)
(2)
(3)
(4)
(5)
(6)
(7)
(8)
(D/ \<2)
:- p,r. :- q(X),!,v,r.
[X/a]
(5)
(!) :- v,r.
fail
• . s.
(7)
□
Hana Rudová, Logické programování I, 9. dubna 2013
14
SLD rezoluce v Prologu
a(X) : -b(X, Y),\,c(Y)
a(X) : -c(X).
b(2, 3).
b(l, 2).
c(2).
s(X) : -a(X). s(X) : -p(X).
p(B) : -q(A,B),r(B). p (A) : -q(A,A). q(a, a). q(a, b). r(b).
Príklad: rez II
(1)
(2)
(3)
(4)
(5)
(6)
(7)
(8)
(9)
(10)
(11)
(12)
:— s(X). (6) /      \ (7)
:— a(X).
:- b(X,Y),!,c(Y). [X/2,Y/3] (3)
:— !,c(3). (rez) :— c(3).
fail
Hana Rudová, Logické programování I, 9. dubna 2013
15
SLD rezoluce v Prologu
a(X) : -b(X,Y),c(Y),!
a(X) : -c(X).
b(2, 3).
b(l, 2).
c(2).
s(X) : -a(X). s(X) : -p(X).
p(B) : -q(A,B),r(B). p (A) : -q(A,A). q(a, a). q(a, b). r(b).
Príklad: rez III
d)
(2)
(3)
(4)
(5)
(6)
(7)
(8)
(9)
(10)
(11)
(12)
:- s(X). (6) /      \(7)
(1l
:- a(X).
:- b(X,Y),c(Y),!. [X/2,Y/3] (3)/    \   (4) [X/1,Y/2]
:- c(3),!.   :- c(2),!.
fail
(5)
• • •
(rez)
□
[X/1]
Hana Rudová, Logické programování I, 9. dubna 2013
16
SLD rezoluce v Prologu
Negace v logickém programování
Negativní znalost
JS> logiCké programy vyjadřují pozitivní znalost
negativní literály: poziCe urCena definid HornovýCh klauzulí => nelze vyvodit negativní informaCi z logiCkého programu
& každý predikát definuje úplnou relaCi
iť negativní literál není logiCkým důsledkem programu
Hana Rudová, LogiCké programování I, 9. dubna 2013
18
NegaCe v logiCkém programování
Negativní znalost
JS> logické programy vyjadrují pozitivní znalost
negativní literály: pozice urcena definicí Hornových klauzulí => nelze vyvodit negativní informaci z logického programu
& každý predikát definuje úplnou relaci
i* negativní literál není logickým dusledkem programu
& relace vyjádreny explicitne v nejmenším Herbrandove modelu
-i- nad(X,Y) : -na(X,Y). na(c,b). nad(X, Y) : -na(X, Z),nad(Z, Y). na(b, a).
J* 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, 9. dubna 2013
18
Negace v logickém programování
Negativní znalost
JS> logické programy vyjadrují pozitivní znalost
negativní literály: pozice urCena definicí Hornových klauzulí => nelze vyvodit negativní informaci z logického programu
j> každý predikát definuje úplnou relaci
i* negativní literál není logickým dusledkem programu
& relace vyjádreny explicitne v nejmenším Herbrandove modelu
-i- nad(X,Y) : -na(X,Y). na(c,b). nad(X, Y) : -na(X, Z),nad(Z, Y). na(b, a).
J* nejmenší Herbranduv model: {na(b,a),na(c, b),nad(b,a),nad(c, b),nad(c,a)}
JS> ani program ani model nezahrnují negativní informaci a a není nad c, a není na c
S* i v realite je negativní informace vyjadrena explicitne zrídka, napr. jízdní rád
Hana Řudová, Logické programování I, 9. dubna 2013
18
Negace v logickém programování
Predpoklad ůzavreného sveta
neexistenCe informaCe Chápána jako opak:
predpoklad ůzavreného sveta (closed world assumption, CWA)
prevzato z databází
urCitý vztah platí poůze když je vyvoditelný z programu.
P \£ A
„odvozovad pravidlo" (A je (uzavrený) term):-— (CWA)
Hana Rudová, LogiCké programování I, 9. dubna 2013
19
NegaCe v logiCkém programování
Predpoklad uzavreného sveta
neexistence informace chápána jako opak:
predpoklad uzavřeného sveta (closed world assumption, CWA)
p r evzato z databází
urcitý vztah platí pouze když je vyvoditelný z programu.
P \£ A
„odvozovací pravidlo" (A je (uzavr 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, 9. dubna 2013
19
Negace v logickém programování
Predpoklad uzavreného sveta
C neexistence informace chápána jako opak:
predpoklad uzavřeného sveta (closed world assumption, CWA)
-í* prevzato 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 urcit, zda pravidlo CWA je aplikovatelné nebo ne ii> CWA v logickém programování obecne nepoužitelná.
JS> „odvozovací pravidlo" (A je (uzavrený) term):
P £ A
(CWA)
A
Hana Rudová, Logické programování I, 9. dubna 2013
19
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úspeš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, 9. dubna 2013
20
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ú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, 9. dubna 2013 20 Negace v logickém programování
Negace jako neúspech (negation as failure)
£ slabší verze CWA: definitívne neúspeš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)
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, abyjejiCh dusledkem byly i negativní literály zúplnení logického programů
Hana Rudová, LogiCké programování I, 9. dubna 2013 20 NegaCe v logiCkém programování
Podstata zúplnení logického programu
prevod všech if prí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)).
Hana Řudová, Logické programování I, 9. dubna 2013
21
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ž alespon jedna z podmínek platí
A tedy pokud žádná z podmínek neplatí, X není nad Y
Hana Rudová, Logické programování I, 9. dubna 2013
21
Negace v logickém programování
Podstata zúplnení logičké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ž alespon 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(X1,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, 9. dubna 2013 21 Negace v logickém programování
Zúplnení programů
Zúplnení programů P je: comp(P) := IFF(P) u CET -í* Základní vlastnosti: *> comp(P) i= P
s do programuje pridána pouze negativní informaCe
Hana Rudová, LogiCké programování I, 9. dubna 2013
22
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 Řudová, Logické programování I, 9. dubna 2013
22
Negace v logickém programování
IF(q, P)
na(Xi,X2) : -3Y(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.
Hana Rudová, Logické programování I, 9. dubna 2013
23
Negace v logickém programování
IF(q, P)
na(Xi,X2) : -3Y(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(t1, . . . ,tn) : —L1, . . . , Lm
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.
Necht' def(q/n) = {C1,Cj}.
Pak formuli IF(q,P) získáme následujícím postupem: q(X1, ...,Xn) : -E(C1) v E(C2) v ---v E(Cj) pro j> 0 a
q(X1,... ,Xn) : - □ pro j = 0 [q/n není v programu P]
Hana Rudová, Logické programování I, 9. dubna 2013
23
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: 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(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, 9. dubna 2013
24
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á definitivne 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, 9. dubna 2013
25
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)
Hana Rudová, Logické programování I, 9. dubna 2013
25
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 existenči definitivne neúspešného SLD-stromu
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, 9. dubna 2013
25
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, 9. dubna 2013
26
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.
Hana Rudová, Logické programování I, 9. dubna 2013 26 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.
stratifikovaný není stratifikovaný
Hana Rudová, Logické programování I, 9. dubna 2013 26 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.
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 S0 u ... u Sk p(...) : -      —q(...),... g P, p g Sk => q g S0 u ... u Sk-1
Hana Rudová, Logické programování I, 9. dubna 2013 26 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, 9. d bna 2013
27
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ý
& stratifikované programy nemusí mít jedineCný 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, 9. dubna 2013 27 Negace v logickém programování
SLDNF rezoluce: úspešné odvození
C NF pravidlo: : - C. má konecne neúspeš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 (strom pro 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, 9. dubna 2013
28
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 (strom pro C je konečne neúspeš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
=> úspešné odvození
Hana Rudová, Logické programování I, 9. dubna 2013
28
Negace v logickém programování
SLDNF rezoluce: neúspešné 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 důkaz pro C
& 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) : -—blokovaný(X). blokovaný(X) : -na(Y,X). na(_, _).
Hana Rudová, Logické programování I, 9. dubna 2013
29
Negace v logickém programování
NF pravidlo:
-c
Pokud máme negativní podcíl ->C v dotazu G, pak hledáme důkaz pro C
& Pokůd existůje vyvrácení C s prázdnoů sůbstitůcí (strom pro C je koneCne úspešný), pak je odvození G (i — C) celkove neúspešné
nahore(X) :     blokov any(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, 9. dubna 2013
29
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).
Hana Řudová, Logické programování I, 9. dubna 2013
30
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 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, 9. dubna 2013 30 Negace v logickém programování
Cvičení: 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, 9. dubna 2013
31
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
(G0; C0),..., (Gt-i, Ci-1), Gt nebo nekonecná posloupnost
(G0;C0), (G1;C1), (G2;C2),...
kde v každém kroku m + 1(m > 0), R vybírá pozitivní literál v Gm a dospívá k Gm+1 obvyklým způsobem.
Hana Rudová, Logické programování I, 9. dubna 2013
32
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-i, Ct-i), Gi
nebo nekonecná posloupnost
(Go, Co), (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+l obvyklým zpusobem.
můuže být:
2. neúspešné
3. blokované: Gt je negativní (napr. —A)
Hana Rudová, Logické programování I, 9. dubna 2013
32
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, 9. dubna 2013
33
Negace v logickém programování
SLDNF rezoluce: pojmy
Úroven cíle
a P normální program, G0 normální cíl, R selekcní pravidlo: úroven cíle G0 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, 9. dubna 2013
33
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 : - Li,..., Lm-i, —A, Lm+i,... ,Ln pak
Hana Rudová, Logické programování I, 9. dubna 2013
34
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-\, —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, 9. dubna 2013
34
Negace v logickém programování
SLDNF rezoluče
P normální program, G0 normální cíl, R selekcní pravidlo:
množina SLDNF odvození a podmnožina neúspešnýčh 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; C0)) . . . ■> {Gii £) i (: - L1> . . . ■> Lm-1> Lm+1> . . . ■> Ln) je
(úspešné) SLDNF odvození číle G0
e oznacuje prázdnou cílovou substituci
Hana Rudová, Logické programování I, 9. dubna 2013 34 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, 9. dubna 2013
35
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)
Hana Rudová, LogiCké programování I, 9. dubna 2013
36
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 důsledkem comp(P)
s implementace SLDNF v Prologu není korektní
Prolog nereší uvázlé SLDNF-odvození (neprázdná substituce) -i- použití bezpecných cílů (negace neobsahuje promenné)
Hana Rudová, Logické programování I, 9. dubna 2013
36
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 důsledkem 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, 9. dubna 2013
36
Negace v logickém programování