Operační a deklarativní semantika
Operační sémantika
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 nějaký cíl G1
odvodit
nějakým rezolučním důkazem ze vstupní množiny P  {G}.
1
tímto výrazem jsou míněny všechny cíle, pro něž zmíněný rezoluční důkaz
existuje.
Hana Rudová, Logické programování I, 16. dubna 2007 2 Sémantiky
Operační sémantika
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 nějaký cíl G1
odvodit
nějakým rezolučním důkazem ze vstupní množiny P  {G}.
1
tímto výrazem jsou míněny všechny cíle, pro něž zmíněný rezoluční důkaz
existuje.
Deklarativní sémantika logického programu P ???
Hana Rudová, Logické programování I, 16. dubna 2007 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.
příklad: F = {{f(a, b) = f (b, a)}, {f(f(a, a), b) = a}}
interpretace I1: D = Z, a := 1, b := -1, f := " + "
Hana Rudová, Logické programování I, 16. dubna 2007 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.
příklad: F = {{f(a, b) = f (b, a)}, {f(f(a, a), b) = a}}
interpretace I1: 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, 16. dubna 2007 3 Sémantiky
Herbrandovy interpretace
Omezení na obor skládající se ze symbolických výrazů tvořených
z predikátových a funkčních symbolů daného jazyka
při zkoumání pravdivosti není nutné uvažovat modely nad všemi interpretacemi
Hana Rudová, Logické programování I, 16. dubna 2007 4 Sémantiky
Herbrandovy interpretace
Omezení na obor skládající se ze symbolických výrazů tvořených
z predikátových a funkčních symbolů daného jazyka
při zkoumání pravdivosti není nutné uvažovat modely nad všemi interpretacemi
Herbrandovo univerzum: množina všech termů bez proměnných, které
mohou být tvořeny funkčními symboly a konstantami daného jazyka
Herbrandova interpretace: libovolná interpretace, která přiřazuje
proměnným prvky Herbrandova univerza
konstantám sebe samé
funkčním symbolům funkce, které symbolu f pro argumenty t1,    , tn přiřadí term
f(t1,    , tn)
predikátovým symbolům libovolnou funkci z Herbrand. univerza do pravdivostních hodnot
Hana Rudová, Logické programování I, 16. dubna 2007 4 Sémantiky
Herbrandovy interpretace
Omezení na obor skládající se ze symbolických výrazů tvořených
z predikátových a funkčních symbolů daného jazyka
při zkoumání pravdivosti není nutné uvažovat modely nad všemi interpretacemi
Herbrandovo univerzum: množina všech termů bez proměnných, které
mohou být tvořeny funkčními symboly a konstantami daného jazyka
Herbrandova interpretace: libovolná interpretace, která přiřazuje
proměnným prvky Herbrandova univerza
konstantám sebe samé
funkčním symbolům funkce, které symbolu f pro argumenty t1,    , tn přiřadí term
f(t1,    , tn)
predikátovým symbolům libovolnou funkci z Herbrand. univerza do pravdivostních hodnot
Herbrandův model množiny uzavřených formulí P:
Herbrandova interpretace taková, že každá formule z P je v ní pravdivá.
Hana Rudová, Logické programování I, 16. dubna 2007 4 Sémantiky
Specifikace Herbrandova modelu
Herbrandovy interpretace mají předdefinovaný význam funktorů a konstant
Pro specifikaci Herbrandovy interpretace tedy stačí zadat
relace pro každý predikátový symbol
Hana Rudová, Logické programování I, 16. dubna 2007 5 Sémantiky
Specifikace Herbrandova modelu
Herbrandovy interpretace mají předdefinovaný význam funktorů a konstant
Pro specifikaci Herbrandovy interpretace tedy stačí zadat
relace pro každý predikátový symbol
Příklad: Herbrandova interpretace a Herbrandův model množiny formulí
lichy(s(0)). % (1)
lichy(s(s(X))) :- lichy(X). % (2)
Hana Rudová, Logické programování I, 16. dubna 2007 5 Sémantiky
Specifikace Herbrandova modelu
Herbrandovy interpretace mají předdefinovaný význam funktorů a konstant
Pro specifikaci Herbrandovy interpretace tedy stačí zadat
relace pro každý predikátový symbol
Příklad: Herbrandova interpretace a Herbrandův model množiny formulí
lichy(s(0)). % (1)
lichy(s(s(X))) :- lichy(X). % (2)
I1 =  není model (1)
Hana Rudová, Logické programování I, 16. dubna 2007 5 Sémantiky
Specifikace Herbrandova modelu
Herbrandovy interpretace mají předdefinovaný význam funktorů a konstant
Pro specifikaci Herbrandovy interpretace tedy stačí zadat
relace pro každý predikátový symbol
Příklad: Herbrandova interpretace a Herbrandův model množiny formulí
lichy(s(0)). % (1)
lichy(s(s(X))) :- lichy(X). % (2)
I1 =  není model (1)
I2 = {lichy(s(0))} není model (2)
Hana Rudová, Logické programování I, 16. dubna 2007 5 Sémantiky
Specifikace Herbrandova modelu
Herbrandovy interpretace mají předdefinovaný význam funktorů a konstant
Pro specifikaci Herbrandovy interpretace tedy stačí zadat
relace pro každý predikátový symbol
Příklad: Herbrandova interpretace a Herbrandův model množiny formulí
lichy(s(0)). % (1)
lichy(s(s(X))) :- lichy(X). % (2)
I1 =  není model (1)
I2 = {lichy(s(0))} není model (2)
I3 = {lichy(s(0)), lichy(s(s(s(0))))} není model (2)
Hana Rudová, Logické programování I, 16. dubna 2007 5 Sémantiky
Specifikace Herbrandova modelu
Herbrandovy interpretace mají předdefinovaný význam funktorů a konstant
Pro specifikaci Herbrandovy interpretace tedy stačí zadat
relace pro každý predikátový symbol
Příklad: Herbrandova interpretace a Herbrandův model množiny formulí
lichy(s(0)). % (1)
lichy(s(s(X))) :- lichy(X). % (2)
I1 =  není model (1)
I2 = {lichy(s(0))} není model (2)
I3 = {lichy(s(0)), lichy(s(s(s(0))))} není model (2)
I4 = {lichy(sn
(0))|n  {1, 3, 5, 7, . . .}} Herbrandův model (1) i (2)
Hana Rudová, Logické programování I, 16. dubna 2007 5 Sémantiky
Specifikace Herbrandova modelu
Herbrandovy interpretace mají předdefinovaný význam funktorů a konstant
Pro specifikaci Herbrandovy interpretace tedy stačí zadat
relace pro každý predikátový symbol
Příklad: Herbrandova interpretace a Herbrandův model množiny formulí
lichy(s(0)). % (1)
lichy(s(s(X))) :- lichy(X). % (2)
I1 =  není model (1)
I2 = {lichy(s(0))} není model (2)
I3 = {lichy(s(0)), lichy(s(s(s(0))))} není model (2)
I4 = {lichy(sn
(0))|n  {1, 3, 5, 7, . . .}} Herbrandův model (1) i (2)
I5 = {lichy(sn
(0))|n  N}} Herbrandův model (1) i (2)
Hana Rudová, Logické programování I, 16. dubna 2007 5 Sémantiky
Příklad: Herbrandovy interpretace
rodic(a,b).
rodic(b,c).
predek(X,Y) :- rodic(X,Y).
predek(X,Z) :- rodic(X,Y), predek(Y,Z).
Hana Rudová, Logické programování I, 16. dubna 2007 6 Sémantiky
Příklad: Herbrandovy interpretace
rodic(a,b).
rodic(b,c).
predek(X,Y) :- rodic(X,Y).
predek(X,Z) :- rodic(X,Y), predek(Y,Z).
I1 = {rodic(a, b), rodic(b, c), predek(a, b), predek(b, c), predek(a, c)}
I2 = {rodic(a, b), rodic(b, c),
predek(a, b), predek(b, c), predek(a, c), predek(a, a)}
I1 i I2 jsou Herbrandovy modely klauzulí
Hana Rudová, Logické programování I, 16. dubna 2007 6 Sémantiky
Deklarativní a operační sémantika
Je-li S množina programových klauzulí a M libovolná množina Herbrandových
modelů S, pak průnik těchto modelů je opět Herbrandův model množiny S.
Důsledek:
Existuje nejmenší Herbrandův model množiny S, který značíme M(S).
Hana Rudová, Logické programování I, 16. dubna 2007 7 Sémantiky
Deklarativní a operační sémantika
Je-li S množina programových klauzulí a M libovolná množina Herbrandových
modelů S, pak průnik těchto modelů je opět Herbrandův model množiny S.
Důsledek:
Existuje nejmenší Herbrandův model množiny S, který značíme M(S).
Deklarativní sémantikou logického programu P rozumíme jeho minimální
Herbrandův model M(P).
Hana Rudová, Logické programování I, 16. dubna 2007 7 Sémantiky
Deklarativní a operační sémantika
Je-li S množina programových klauzulí a M libovolná množina Herbrandových
modelů S, pak průnik těchto modelů je opět Herbrandův model množiny S.
Důsledek:
Existuje nejmenší Herbrandův model množiny S, který značíme M(S).
Deklarativní sémantikou logického programu P rozumíme jeho minimální
Herbrandův model M(P).
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 nějaký cíl G1
odvodit
nějakým rezolučním důkazem ze vstupní množiny P  {G}.
1
tímto výrazem jsou míněny všechny cíle, pro něž zmíněný rezoluční důkaz
existuje.
Hana Rudová, Logické programování I, 16. dubna 2007 7 Sémantiky
Deklarativní a operační sémantika
Je-li S množina programových klauzulí a M libovolná množina Herbrandových
modelů S, pak průnik těchto modelů je opět Herbrandův model množiny S.
Důsledek:
Existuje nejmenší Herbrandův model množiny S, který značíme M(S).
Deklarativní sémantikou logického programu P rozumíme jeho minimální
Herbrandův model M(P).
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 nějaký cíl G1
odvodit
nějakým rezolučním důkazem ze vstupní množiny P  {G}.
1
tímto výrazem jsou míněny všechny cíle, pro něž zmíněný rezoluční důkaz
existuje.
Pro libovolný logický program P platí M(P) = O(P)
Hana Rudová, Logické programování I, 16. dubna 2007 7 Sémantiky
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
Hana Rudová, Logické programování I, 16. dubna 2007 9 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).
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, 16. dubna 2007 9 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).
nejmenší 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 vyjadřena explicitně zřídka, např. jízdní řád
Hana Rudová, Logické programování I, 16. dubna 2007 9 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í
určitý vztah platí pouze když je vyvoditelný z programu.
,,odvozovací pravidlo" (A je (uzavřený) term):
P A
A
(CWA)
Hana Rudová, Logické programování I, 16. dubna 2007 10 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í
určitý vztah platí pouze když je vyvoditelný z programu.
,,odvozovací pravidlo" (A je (uzavřený) term):
P A
A
(CWA)
pro SLD-rezoluci: P nad(a, c), tedy lze podle CWA odvodit nad(a, c)
Hana Rudová, Logické programování I, 16. dubna 2007 10 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í
určitý vztah platí pouze když je vyvoditelný z programu.
,,odvozovací pravidlo" (A je (uzavřený) term):
P A
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 CWA je aplikovatelné nebo ne
CWA v logickém programování obecně nepoužitelná.
Hana Rudová, Logické programování I, 16. dubna 2007 10 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, 16. dubna 2007 11 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).
rozdíl mezi CWA a NF
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 nekonečný
existuje odvození cíle podle CWA, protože neexistuje vyvrácení : -nad(b, c)
Hana Rudová, Logické programování I, 16. dubna 2007 11 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).
rozdíl mezi CWA a NF
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 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, 16. dubna 2007 11 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))  (na(X, Z), nad(Z, Y)).
zúplnění: nad(X, Y)  (na(X, Y))  (na(X, Z), nad(Z, Y)).
Hana Rudová, Logické programování I, 16. dubna 2007 12 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))  (na(X, Z), nad(Z, Y)).
zúplnění: nad(X, Y)  (na(X, Y))  (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
Hana Rudová, Logické programování I, 16. dubna 2007 12 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))  (na(X, Z), nad(Z, Y)).
zúplnění: nad(X, Y)  (na(X, Y))  (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(X1, X2) : -X1 = c, X2 = b.
na(X1, X2) : -X1 = b, X2 = a.
zúplnění: na(X1, X2) : -(X1 = c, X2 = b)  (X1 = b, X2 = a).
Hana Rudová, Logické programování I, 16. dubna 2007 12 Negace v logickém programování
Zúplnění programu
Zúplnění programu P je: comp(P) := IFF(P)  CET
Základní vlastnosti:
comp(P) P
do programu je přidána pouze negativní informace
Hana Rudová, Logické programování I, 16. dubna 2007 13 Negace v logickém programování
Zúplnění programu
Zúplnění programu P je: comp(P) := IFF(P)  CET
Základní vlastnosti:
comp(P) P
do programu je 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
def(p/n) predikátu p/n množina všech klauzulí predikátu p/n
Hana Rudová, Logické programování I, 16. dubna 2007 13 Negace v logickém programování
IF(q, P)
na(X1, X2) : -Y(X1 = c, X2 = b, f(Y))  (X1 = b, X2 = a, g).
na(c, b) : -f(Y). na(b, a) : -g.
q/n predikátový symbol programu P
X1, . . . , Xn jsou ,,nové" proměnné, 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 označme E(C) výraz Y1, . . . , Yk(X1 = t1, . . . , Xn = tn, L1, . . . , Lm)
kde Y1, . . . , Yk jsou všechny proměnné v C.
Hana Rudová, Logické programování I, 16. dubna 2007 14 Negace v logickém programování
IF(q, P)
na(X1, X2) : -Y(X1 = c, X2 = b, f(Y))  (X1 = b, X2 = a, g).
na(c, b) : -f(Y). na(b, a) : -g.
q/n predikátový symbol programu P
X1, . . . , Xn jsou ,,nové" proměnné, 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 označme E(C) výraz Y1, . . . , Yk(X1 = t1, . . . , Xn = tn, L1, . . . , Lm)
kde Y1, . . . , Yk jsou všechny proměnné v C.
Necht' def(q/n) = {C1, . . . , Cn}.
Pak formuli IF(q, P) získáme následujícím postupem:
q(X1, . . . , Xn) : -E(C1)  E(C2)      E(Cj) pro j > 0 a
q(X1, . . . , Xn) : - pro j = 0 [q/n není v programu P]
Hana Rudová, Logické programování I, 16. dubna 2007 14 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 = Y  Y = Z  X = Z
4. pro každý f/m: X1 = Y1      Xm = Ym  f(X1, . . . , Xm) = f(Y1, . . . , Ym)
5. pro každý p/m: X1 = Y1      Xm = Ym  (p(X1, . . . , Xm)  p(Y1, . . . , Ym))
6. pro všechny různé f/m a g/n, (m, n  0): f(X1, . . . , Xm) = g(Y1, . . . , Yn)
7. pro každý f/m: f(X1, . . . , Xm) = f(Y1, . . . , Ym)  X1 = Y1      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, 16. dubna 2007 15 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á definitivně neúspěšný SLD-strom,
pak (A) je logickým důsledkem comp(P) (nebo-li comp(P) (A))
Hana Rudová, Logické programování I, 16. dubna 2007 16 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á definitivně neúspěšný SLD-strom,
pak (A) je logickým důsledkem comp(P) (nebo-li comp(P) (A))
Úplnost NF pravidla: Necht' P je logický program. Jestliže comp(P) (A),
pak existuje definitivně neúspěšný SLD-strom : -A.
zůstává problém: není rozhodnutelné, zda daná atomická formule je logickým důsledkem
daného logického programu.
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)
Hana Rudová, Logické programování I, 16. dubna 2007 16 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á definitivně neúspěšný SLD-strom,
pak (A) je logickým důsledkem comp(P) (nebo-li comp(P) (A))
Úplnost NF pravidla: Necht' P je logický program. Jestliže comp(P) (A),
pak existuje definitivně neúspěšný SLD-strom : -A.
zůstává problém: není rozhodnutelné, zda daná atomická formule je logickým důsledkem
daného logického programu.
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) (A)) je A všeob. kvantifikováno, v (A) nejsou volné proměnné
Hana Rudová, Logické programování I, 16. dubna 2007 16 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  p
rozdělení programu na vrstvy
vynucují použití negace relace pouze tehdy pokud je relace úplně definovaná
Hana Rudová, Logické programování I, 16. dubna 2007 17 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  p
rozdělení programu na vrstvy
vynucují použití negace relace pouze tehdy pokud je relace úplně definovaná
a. a.
a : -b, a. a : -b, a.
b. b : -a.
Hana Rudová, Logické programování I, 16. dubna 2007 17 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  p
rozdělení programu na vrstvy
vynucují použití negace relace pouze tehdy pokud je relace úplně definovaná
a. a.
a : -b, a. a : -b, a.
b. b : -a.
stratifikovaný není stratifikovaný
Hana Rudová, Logické programování I, 16. dubna 2007 17 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  p
rozdělení programu na vrstvy
vynucují použití negace relace pouze tehdy pokud je relace úplně 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 symbolů
programu lze rozdělit do disjunktních množin S0, . . . , Sm (Si  stratum)
p(. . .) : - . . . , q(. . .), . . .  P, p  Sk = q  S0  . . .  Sk
p(. . .) : - . . . , q(. . .), . . .  P, p  Sk = q  S0  . . .  Sk-1
Hana Rudová, Logické programování I, 16. dubna 2007 17 Negace v logickém programování
Stratifikované programy II
program je m-stratifikovaný  m je nejmenší index takový,
že S0  . . .  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ý
Hana Rudová, Logické programování I, 16. dubna 2007 18 Negace v logickém programování
Stratifikované programy II
program je m-stratifikovaný  m je nejmenší index takový,
že S0  . . .  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
cykli : -zastavi.
dva minimální Herbrandovy modely: {cykli}, {zastavi}
důsledek toho, že cykli : -zastavi. je ekvivalentní cykli  zastavi
Hana Rudová, Logické programování I, 16. dubna 2007 18 Negace v logickém programování
SLDNF rezoluce: úspěšné odvození
NF pravidlo: : - C. má konečně neúspěšný SLD-strom
C
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) : -blokovany(X).
blokovany(X) : -na(Y, X).
na(a, b).
Hana Rudová, Logické programování I, 16. dubna 2007 19 Negace v logickém programování
SLDNF rezoluce: úspěšné odvození
NF pravidlo: : - C. má konečně neúspěšný SLD-strom
C
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) : -blokovany(X).
blokovany(X) : -na(Y, X).
na(a, b).
: -nahore(c).
yes
FAIL
:- nahore(c). :- blokovany(c).
:- na(Y,c).:- blokovany(c).
 uspěšné odvození
Hana Rudová, Logické programování I, 16. dubna 2007 19 Negace v logickém programování
SLDNF rezoluce: neúspěšné odvození
NF pravidlo: : - C. má konečně neúspěšný SLD-strom
C
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) : -blokovany(X).
blokovany(X) : -na(Y, X).
na(_, _).
Hana Rudová, Logické programování I, 16. dubna 2007 20 Negace v logickém programování
SLDNF rezoluce: neúspěšné odvození
NF pravidlo: : - C. má konečně neúspěšný SLD-strom
C
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) : -blokovany(X).
blokovany(X) : -na(Y, X).
na(_, _).
: -nahore(X).
no
:- nahore(X).
:- blokovany(X).
:- blokovany(X).
:- na(Y,X).
 neúspěšné odvození
Hana Rudová, Logické programování I, 16. dubna 2007 20 Negace v logickém programování
SLDNF rezoluce: uvázlé odvození
NF pravidlo: : - C. má konečně neúspěšný SLD-strom
C
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) : -blokovany(X).
blokovany(X) : -na(Y, X).
na(a, b).
Hana Rudová, Logické programování I, 16. dubna 2007 21 Negace v logickém programování
SLDNF rezoluce: uvázlé odvození
NF pravidlo: : - C. má konečně neúspěšný SLD-strom
C
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) : -blokovany(X).
blokovany(X) : -na(Y, X).
na(a, b).
: -nahore(X).
[Y/a,X/b]
[X/b]
:- nahore(X).
:- blokovany(X).
:- blokovany(X).
:- na(Y,X).
 uvázlé odvození
Hana Rudová, Logické programování I, 16. dubna 2007 21 Negace v logickém programování
SLD+
odvození
P je normální program, G0 normální cíl, R selekční pravidlo:
SLD+
-odvození G0 je bud' konečná posloupnost
G0; C0 , . . . , Gi-1; Ci-1 , Gi
nebo nekonečná 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, 16. dubna 2007 22 Negace v logickém programování
SLD+
odvození
P je normální program, G0 normální cíl, R selekční pravidlo:
SLD+
-odvození G0 je bud' konečná posloupnost
G0; C0 , . . . , Gi-1; Ci-1 , Gi
nebo nekonečná 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.
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, 16. dubna 2007 22 Negace v logickém programování
SLDNF rezoluce: pojmy
Úroveň cíle
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
k + 1  maximální úroveň cílů : -A,
které ve tvaru A blokují SLD+
-odvození G0, je k
nekonečná úroveň cíle: blokované SLDNF odvození
Hana Rudová, Logické programování I, 16. dubna 2007 23 Negace v logickém programování
SLDNF rezoluce: pojmy
Úroveň cíle
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
k + 1  maximální úroveň cílů : -A,
které ve tvaru A blokují SLD+
-odvození G0, je k
nekonečná úroveň cíle: blokované SLDNF odvození
Množina SLDNF odvození = {(SLDNF odvození G0)  (SLDNF odvození : -A)}
při odvozování G0 jsme se dostali k cíli A
SLDNF odvození cíle G ?
Hana Rudová, Logické programování I, 16. dubna 2007 23 Negace v logickém programování
SLDNF rezoluce
P normální program, G0 normální cíl, R selekční pravidlo:
množina SLDNF odvození a podmnožina neúspěš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í G0; C0 , . . . , Gi blokováno na A
tj. Gi je tvaru : - L1, . . . , Lm-1, A, Lm+1, . . . , Ln
pak
Hana Rudová, Logické programování I, 16. dubna 2007 24 Negace v logickém programování
SLDNF rezoluce
P normální program, G0 normální cíl, R selekční pravidlo:
množina SLDNF odvození a podmnožina neúspěš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í G0; C0 , . . . , Gi blokováno na A
tj. Gi je tvaru : - L1, . . . , Lm-1, A, Lm+1, . . . , Ln
pak
existuje-li SLDNF odvození : -A (pod R) s prázdnou cílovou substitucí, pak
G0; C0 , . . . , Gi je neúspěšné SLDNF odvození
Hana Rudová, Logické programování I, 16. dubna 2007 24 Negace v logickém programování
SLDNF rezoluce
P normální program, G0 normální cíl, R selekční pravidlo:
množina SLDNF odvození a podmnožina neúspěš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í G0; C0 , . . . , Gi blokováno na A
tj. Gi je tvaru : - L1, . . . , Lm-1, A, Lm+1, . . . , Ln
pak
existuje-li SLDNF odvození : -A (pod R) s prázdnou cílovou substitucí, pak
G0; C0 , . . . , Gi je neúspěšné SLDNF odvození
je-li každé úplné SLDNF odvození : -A (pod R) neúspěšné pak
G0; C0 , . . . , Gi, , (: - L1, . . . , Lm-1, Lm+1, . . . , Ln) je
(úspěšné) SLDNF odvození cíle G0
označuje prázdnou cílovou substituci
Hana Rudová, Logické programování I, 16. dubna 2007 24 Negace v logickém programování
SLDNF rezoluce
P normální program, G0 normální cíl, R selekční pravidlo:
množina SLDNF odvození a podmnožina neúspěš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í G0; C0 , . . . , Gi blokováno na A
tj. Gi je tvaru : - L1, . . . , Lm-1, A, Lm+1, . . . , Ln
pak
existuje-li SLDNF odvození : -A (pod R) s prázdnou cílovou substitucí, pak
G0; C0 , . . . , Gi je neúspěšné SLDNF odvození
je-li každé úplné SLDNF odvození : -A (pod R) neúspěšné pak
G0; C0 , . . . , Gi, , (: - L1, . . . , Lm-1, Lm+1, . . . , Ln) je
(úspěšné) SLDNF odvození cíle G0
označuje prázdnou cílovou substituci
Hana Rudová, Logické programování I, 16. dubna 2007 24 Negace v logickém programování
Typy SLDNF odvození
Konečné SLDNF-odvození může být:
1. úspěšné: Gi =
2. neúspěšné
3. uvázlé (flounder):
Gi je negativní (A) a : -A je úspěšné s neprázdnou cílovou substitucí
4. blokované: Gi je negativní (A) a : -A nemá konečnou úroveň.
Hana Rudová, Logické programování I, 16. dubna 2007 25 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  cílová substituce SLDNF-odvození cíle : -G, pak
G je logickým důsledkem comp(P)
Hana Rudová, Logické programování I, 16. dubna 2007 26 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  cílová substituce SLDNF-odvození cíle : -G, pak
G 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é)
Hana Rudová, Logické programování I, 16. dubna 2007 26 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  cílová substituce SLDNF-odvození cíle : -G, pak
G 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 A platí
ale místo toho se odvozování : -A může zacyklit, tj. SLDNF rezoluce A neodvodí
 A tedy sice platí, ale SLDNF rezoluce ho nedokáže odvodit
Hana Rudová, Logické programování I, 16. dubna 2007 26 Negace v logickém programování