Rezoluce a logické programování
(pokračování)
Příklad: SLD-strom a výsledná substituce
: -a(Z).
a(X) : -b(X,Y),c(Y) a(X) : -c(X). b(2, 3). b(l, 2). c(2).
(1)
(2)
(3)
(4)
(5)
:- a(Z). (1)/ \(2)
:- b(Z,Y), c(Y).        :- c(Z). [Z/2,Y/3] (3) / \4) [Z/1,Y/2]       \ (5) [Z/2]
:- c(3).
fall
:- c(2). (5)
□
[Z/1]
□
[Z/2]
Hana Rudová, Logické programování I, 11. dubna 2012
2
Rezoluce a logické programování
Příklad: SLD-strom a výsledná substituce
: -a(Z).
a(X) : -b(X,Y),c(Y) a(X) : -c(X). b(2, 3). b(l, 2). c(2).
Cvičení:
p(B) : -q(A,B),r(B). p (A) : -q(A,A). q(a, a). q(a, b). r(b).
(1)
(2)
(3)
(4)
(5)
:- a(Z). (1)/ \(2)
:- b(Z,Y), c(Y).        :- c(Z). [Z/2,Y/3] (3) / \4) [Z/1,Y/2]       \ (5) [Z/2]
:- c(3).
fail
:- c(2). (5)
□
[Z/1]
□
[Z/2]
ve výsledné substituci jsou pouze proměnné z dotazu, tj. výsledné substituce jsou [Z/l] a [Z/2] nezajímá me substituce [Y/2]
Hana Rudová, Logické programování I, 11. dubna 2012
2
Rezoluce a logické programování
Výsledná substituce (answer substitution)
q(a).                        —       P(X,Y).      q(a). [X/a]
p(a,b). I /
:- p(a,Y).   p(a,b). [Y/b]
:-q(X), p(X,Y). /
X=a, Y=b                                  □ [X/a,Y/b]
Hana Rudová, Logické programování I, 11. dubna 2012
3
Rezoluce a logické programování
Výsledná substituce (answer substitution)
q(a). —        P(X,Y).      q(a). [X/a]
p(a,b). I /
:- p(a,Y).   p(a,b). [Y/b]
:-q(X), p(X,Y). /
X=a, Y=b □ [X/a,Y/b]
JS> Každý krok SLD-rezoluce vytváří novou unifikacní substituci Qi
=> potenciální instanciace proměnné ve vstupní cílové klauzuli
& Výsledná substituce (answer substitution)
Q = QqQi • • • Qn složení unifikací
Hana Rudová, Logické programování I, 11. dubna 2012
3
Rezoluce a logické programování
Význam SLD-rezolučního vyvrácení P u {G}
M Množina P programových klauzulí, cílová klauzule G
& Dokazujeme nesplnitelnost
(1) P A (VX)(-Gi(X) v -Gz(X) v - -- v -Gn(X))
kde G = { — Gi, -G2, - - - , — Gn} a X je vektor proměnných v G
Hana Rudová, Logické programování I, 11. dubna 2012
4
Rezoluce a logické programování
Význam SLD-rezolučního vyvrácení P u {G}
M Množina P programových klauzulí, cílová klauzule G & Dokazujeme nesplnitelnost
(1) P A (VX)(-Gi(X) v -Gz(X) v - -- v -Gn(X))
kde G = { — Gi, -G2, - - - , — Gn} a X je vektor proměnných v G nesplnitelnost (1) je ekvivalentní tvrzení (2) a (3)
(2) P v- —G
(3) P h (3X)(Gi(X) A--- A Gn(X))
Hana Rudová, Logické programování I, 11. dubna 2012
4
Rezoluce a logické programování
Význam SLD-rezolučního vyvrácení P u {G}
M Množina P programových klauzulí, cílová klauzule G & Dokazujeme nesplnitelnost
(1) P A (VX)(-Gi(X) v -Gz(X) v - -- v -Gn(X))
kde G = { — Gi, —G2, - - - , — Gn} a X je vektor proměnných v G nesplnitelnost (1) je ekvivalentní tvrzení (2) a (3)
(2) P v- —G
(3) P h (3X)(Gi(X) A--- A Gn(X))
a jedná se tak o dUkaz existence vhodných objektu, které na základe vlastností množiny P splnují konjunkci literálu v cílové klauzuli
Hana Rudová, Logické programování I, 11. dubna 2012
4
Rezoluce a logické programování
Význam SLD-rezolučního vyvrácení P u {G}
M Množina P programových klauzulí, cílová klauzule G & Dokazujeme nesplnitelnost
(1) P A (VX)(-Gi(X) v -Gz(X) v - -- v -Gn(X))
kde G = { — Gi, —G2, - - - , — Gn} a X je vektor proměnných v G nesplnitelnost (1) je ekvivalentní tvrzení (2) a (3)
(2) P v- —G
(3) P h (3X)(Gi(X) A--- A Gn(X))
a jedná se tak o dUkaz existence vhodných objektu, které na základe vlastností množiny P splnují konjunkci literálu v cílové klauzuli
-i* Dukaz nesplnitelnosti P u {G} znamená nalezení protipříkladu
ten pomocí SLD-stromu konstruuje termy (odpoveď) splnující konjunkci v (3)
Hana Rudová, Logické programování I, 11. dubna 2012
4
Rezoluce a logické programování
Výpočetní strategie
Korektní výpočetní strategie prohledávání stromu výpočtu musí zaručit, že se každý (konečný) výsledek nalézt v konečném čase
Hana Rudová, Logičké programování I, 11. dubna 2012
5
Rezoluče a logičké programování
Výpočetní strategie
Korektní výpočetní strategie prohledávání stromu výpočtu musí zaručit, že se každý (konečný) výsledek nalézt v konečném čase
& Korektní výpočetní strategie = prohledávání stromu do šírky
& exponenčiální pamet'ová náročnost a složité rídíčí struktury
Hana Rudová, Logičké programování I, 11. dubna 2012
5
Rezoluče a logičké programování
Výpočetní strategie
Korektní výpočetní strategie prohledávání stromu výpočtu musí zaručit, že se každý (konečný) výsledek nalézt v konečném čase
& Korektní výpočetní strategie = prohledávání stromu do šírky
& exponenčiální pamet'ová náročnost a složité rídíčí struktury
JS> Použitelná výpočetní strategie = prohledávání stromu do hloubky
& jednodučhé rídíčí struktury (zásobník) * lineární pamet'ová náročnost
s> není ale úplná: nenalezne vyvráčení i když existuje
pročházení nekonečné vetve stromu výpočtu => na nekonečnýčh stromečh dojde k začyklení nedostaneme se tak na jiné existujíčí úspešné uzly
Hana Rudová, Logičké programování I, 11. dubna 2012 5 Rezoluče a logičké programování
SLD-rezoluce v Prologu: úplnost
-í* Prolog: prohledávání stromu do hloubky
=> neúplnost použité výpočetní 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, 11. dubna 2012
6
Rezoluce a logické programování
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á
Hana Rudová, Logické programování I, 11. dubna 2012
7
Rezoluce a logické programování
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-i,Xn-i)
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 Rudová, Logické programování I, 11. dubna 2012 7 Rezoluce a logické programování
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í
Hana Rudová, Logické programování I, 11. dubna 2012
8
Rezoluce a logické programování
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, 11. dubna 2012
8
Rezoluce a logické programování
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)
-í* Rešení: problém typu (2) převést na problém typu (1) ?
Hana Rudová, Logické programování I, 11. dubna 2012
8
Rezoluce a logické programování
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)
Reš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 Rudová, Logické programování I, 11. dubna 2012
8
Rezoluce a logické programování
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)
Reš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 R dová, Logické programování I, 11. d bna 2012
Rezoluce a logické programování
8
Ří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
ořezání
Hana Rudová, Logické programování I, 11. dubna 2012
9
Rezoluce a logické programování
Ří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 při backtrackingu) a vracím se přes řez => vracím se až na rodiCe : -p. a zkouším další vetev
Hana Rudová, Logické programování I, 11. dubna 2012
9
Rezoluce a logické programování
Rízení implementače: rez
r ez se syntaktičky čhová jako kterýkoliv jiný literál nemá ale žádnou deklarativní sémantiku místo toho mení implementači programu
p : -q, !,v. snažíme se splnit q
pokud uspeji
=> p reskočím rez a pokračuji 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á, Logičké programování I, 11. dubna 2012
9
Rezoluče a logičké programování
Príklad: rez
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
(!) :— v, r.
fail
(7)
□
Hana Rudová, Logické programování I, 11. dubna 2012
10
Rezoluce a logické programování
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, 11. dubna 2012
11
Rezoluce a logické programování
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, 11. dubna 2012
12
Rezoluce a logické programování
OperaCní 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 nejaký cíl G1 odvodit nejakým rezolucním dukazem ze vstupní množiny P u {Q}.
ltímto výrazem jsou míneny všechny cíle, pro než zmínený rezolucní dukaz existuje.
Hana Rudová, Logické programování I, 11. dubna 2012
14
Sémantiky
OperaCní sémantika
OperaCní 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í důkaz existuje.
iS* Deklarativní sémantika logického programu P ???
Hana Rudová, Logické programování I, 11. dubna 2012
14
Sémantiky
Opakování: interpretace
-i* 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, 11. dubna 2012
15
Sémantiky
Opakování: interpretace
-i* 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 := " + "
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, 11. dubna 2012
15
Sémantiky
Herbrandovy interpretace
& Omezení na obor skládající se ze symbolických výrazu tvorených z predikátových a funkcních symbolu daného jazyka
i* pri zkoumání pravdivosti není nutné uvažovat modely nad všemi interpretacemi
Hana Rudová, Logické programování I, 11. dubna 2012
16
Sémantiky
Herbrandovy interpretače
Omezení na obor skládajíčí se ze symboličkýčh výrazu tvorenýčh z predikátovýčh a funkčníčh symbolu daného jazyka
i* p r i zkoumání pravdivosti není nutné uvažovat modely nad všemi interpretačemi
Herbrandovo univerzum: množina všečh termu bez promennýčh, které mohou být tvo r eny funkčními symboly a konstantami daného jazyka
Herbrandova interpretače: libovolná interpretače, která p r i razuje
i* promenným prvky Herbrandova univerza Jť konstantám sebe samé
J* funkčním symbolum funkče, které symbolu f pro argumenty t1, • • • ,tn p r i radí term
f(tl, • • • ,tn)
J* predikátovým symbolům libovolnou funkči z Herbrand. univerza do pravdivostníčh hodnot
Hana Rudová, Logičké programování I, 11. dubna 2012
16
Sémantiky
Herbrandovy interpretace
& Omezení na obor skládající se ze symbolických výrazu tvorených z predikátových a funkcních symbolu daného jazyka
i* pri zkoumání pravdivosti není nutné uvažovat modely nad všemi interpretacemi
JS> Herbrandovo univerzum: množina všech termu bez promenných, které mohou být tvoreny funkcními symboly a konstantami daného jazyka
i* promenným prvky Herbrandova univerza Jť konstantám sebe samé
J* funkcním symbolum funkce, které symbolu f pro argumenty ti, • • • ,tn priradí term
f(tl, • • • ,tn)
J* predikátovým symbolum libovolnou funkci z Herbrand. univerza do pravdivostních hodnot
& Herbranduv 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, 11. dubna 2012
16
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
Hana Rudová, Logické programování I, 11. dubna 2012
17
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)
Hana Rudová, Logické programování I, 11. dubna 2012
17
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
& Pří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, 11. dubna 2012
17
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)
& li = 0 není model (1)
a l2 = {lichy(s(0))} není model (2)
Hana Rudová, Logické programování I, 11. dubna 2012
17
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 Herbranduv model množiny formulí
1ichy(s(0)). % (1)
1ichy(s(s(X))) :- lichy(X). % (2)
a Ii = 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, 11. dubna 2012
17
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)
& li = 0 není model (1)
a l2 = {lichy(s(0))} není model (2)
13 = {lichy(s(0)), lichy(s(s(s(0))))} není model (2)
14 = {lichy (sn(0))\n e {i, 3, 5, 7,...}} Herbranduv model (1) i (2)
Hana Rudová, Logické programování I, 11. dubna 2012
17
Sémantiky
Specifikace Herbrandova modelu
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 Herbranduv 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,...}} Herbranduv model (1) i (2)
15 = (lichy(sn(0))\n e N}} Herbranduv model (1) i (2)
Hana Rudová, Logické programování I, 11. dubna 2012
17
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, 11. dubna ZClZ
is
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).
1\ = {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)}
1\ i 12 jsou Herbrandovy modely klauzulí
Cvičení: 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, 11. dubna 2012
18
Sémantiky
a operační sémantika
ii> Je-li S množina programovýčh klauzulí a M libovolná množina Herbrandovýčh modelu S, pak průnik tečhto modelů je opet Herbrandův model množiny S.
JS> Důsledek:
Existuje nejmenší Herbrandův model množiny S, který značíme M(S).
Hana Rudová, Logičké programování I, 11. dubna 2012
19
Sémantiky
a operační sémantika
ii> Je-li S množina programových klauzulí a M libovolná množina Herbrandových modelů 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).
Hana Rudová, Logické programování I, 11. dubna 2012
19
Sémantiky
a operacní sémantika
ii> Je-li S množina programových klauzulí a M libovolná množina Herbrandových modelů S, pak prunik techto modelu je opet Herbrandův model množiny S.
JS> Dusledek:
Existuje nejmenší Herbranduv 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 proměnný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í důkaz existuje.
Hana Rudová, Logické programování I, 11. dubna 2012
19
Sémantiky
a operační sémantika
ii> Je-li S množina programovýčh klauzulí a M libovolná množina Herbrandovýčh modelu S, pak průnik tečhto modelů je opet Herbrandův model množiny S.
JS> Důsledek:
Existuje nejmenší Herbrandův model množiny S, který značíme M(S).
-á* Deklarativní sémantikou logičkého programu P rozumíme jeho minimální Herbrandův model M(P).
& Pripomenutí: Operační sémantikou logičkého programu P rozumíme
množinu O(P) všečh atomičkýčh formulí bez promennýčh, které lze pro nejaký číl Q1 odvodit nejakým rezolučním dukazem ze vstupní množiny P u {Q}.
1tímto výrazem jsou míneny všečhny číle, pro než zmínený rezoluční dukaz existuje.
-i* Pro libovolný logičký program P platí      M(P) = O(P)
Hana Rudová, Logičké programování I, 11. dubna 2012
19
Sémantiky