Rezoluce a logické programování
(pokračování)
Uspořádané klauzule (definite clauses)
M Klauzule = množina literálu
M Uspořádaná klauzule (definite clause) = posloupnost literálu
3 nelze volně měnit pořadí literálu
M Rezoluční princip pro uspořádané klauzule:
______{^A0,...,^An}_______{£, ^£0,...,^£m}______
{^A0,..., -"Aí-i, ^B0p, ..., -*Bmp,-iAi+i,..., ^An}a
3 uspořádaná rezolventa: {^A0,..., -"Aí-i, ^£oP,..., -^Bmp,^Ai+i,..., -^An}<j
3 p je přejmenování proměnných takové, že klauzule {A0,...,An} a {5,50,... ,Bm}p nemají společné proměnné
3 a je nejobecnější unifikátor pro Ai a Bp
Hana Rudová, Logické programování I, 1 4. dubna 201 0
2
Rezoluce a logické programování
Uspořádané klauzule (definite clauses)
M Klauzule = množina literálu
M Uspořádaná klauzule (definite clause) = posloupnost literálu
3 nelze volně měnit pořadí literálu
M Rezoluční princip pro uspořádané klauzule:
______{^A0,...,^An}_______{£, ^£0,...,^£m}______
{^A0,..., -"Aí-i, ^B0p, ..., -*Bmp,-iAi+i,..., ^An}a
3 uspořádaná rezolventa: {^A0,..., ^Aj_i, ^£oP,..., -^Bmp,^Ai+i,..., -^An}<j
3 p je přejmenování proměnných takové, že klauzule {A0,...,An} a {5,50,... ,Bm}p nemají společné proměnné
3 a je nejobecnější unifikátor pro Ai a Bp
3 rezoluce je realizována na literátech ~^Aí<j aBpa
3 je dodržováno pořadí literálu, tj.
{^Bop,..., -^Bmp}<j jde do uspořádané rezolventy přesně na pozici ^AjCr
Hana Rudová, Logické programování I, 14. dubna 2010                       2                                                              Rezoluce a logické programování
Uspořádané klauzule IL
-• Uspořádané klauzule
______{^A0,...,^An}_______{£, ^£0,...,^£m}______
{^A0,..., -"Aí-i, ^B0p, ..., -'5mpl-iAí+il..., ^An}a
Hornovy klauzule
■ — Ao, ■ ■ ■ , An.             i) . —-Do? ■ ■ ■ j -Dm-
: -(Aq, ...,Aí_i,EoPi ■ ■ ■ ,Bmp,Ai+i,... ,An)a.
Hana Rudová, Logické programování I, 14. dubna 2010                       3                                                              Rezoluce a logické programování
Uspořádané klauzule IL
-• Uspořádané klauzule
______{^A0,...,^An}______{£, ^£0,...,^£m}______
{^A0,..., -"Aí-i, ^B0p, ..., -'5mpl-iAí+il..., ^An}a
Hornovy klauzule
■ — Ao, ■ ■ ■ , An.             i) . —-Do? ■ ■ ■ j -Dm-
: -(Ao,...,Aí_i,EoPi ■ ■ ■ ,Bmp,Ai+i,... ,An)a. M Příklad:
ln5tf),nt(l),nMffl}        { t (Z) , ig (Z, X) ^T ( 3 ) }
{-.5(X),--íí(l,A),-.r(3),-.u(X)}
: -5(X),r(l),u(X).       r(Z) : -q(Z,X),r(3). :-s(X),qa,A),r(3)MX).
p = [X/A]       a = [Z/l]
Hana Rudová, Logické programování I, 1 4. dubna 201 0
3
Rezoluce a logické programování
LD-rezoluce
M LD-rezoluční vyvrácení množiny uspořádaných klauzulí P u {G} je posloupnost (Go, Co), ■ ■ ■, {Gn, Cn) taková, že
M Gi,Cijsou uspořádané klauzule M G = Go
«•  Gn+l = D
-• Gt je uspořádaná cílová klauzule -• Ci je přejmenování klauzule z P
& Ci neobsahuje proměnné, které jsou v Gj, j < i nebo v Q, k < i
M Gi+1,0 < í < nje uspořádaná rezolventa Gi a Ci
Hana Rudová, Logické programování I, 1 4. dubna 201 0
4
Rezoluce a logické programování
LD-rezoluce
M LD-rezoluční vyvrácení množiny uspořádaných klauzulí P u {G} je posloupnost (Go, Co), ■ ■ ■, {Gn, Cn) taková, že
M Gi,Cijsou uspořádané klauzule M G = Go
«•  Gn+l = D
-• Gt je uspořádaná cílová klauzule -• Ci je přejmenování klauzule z P
& Ci neobsahuje proměnné, které jsou v Gj, j < i nebo v Q, k < i
M Gi+1,0 < í < nje uspořádaná rezolventa Gi a Ci ^ LD-rezoluce: korektní a úplná
Hana Rudová, Logické programování I, 14. dubna 2010                       4                                                              Rezoluce a logické programování
SLD-rezoluce
-• Lineární rezoluce se selekčním pravidlem     =   SLD-rezoluce (Selected Linear resolution for Definite clauses)
3  rezoluce
M  Selekční pravidlo
M  Lineární rezoluce
-•  Definite (uspořádané) klauzule
M  vstupní rezoluce
Hana Rudová, Logické programování I, 1 4. dubna 201 0
5
Rezoluce a logické programování
SLD-rezoluce
-• Lineární rezoluce se selekčním pravidlem     =   SLD-rezoluce (Selected Linear resolution for Definite clauses)
3  rezoluce
M  Selekční pravidlo
M  Lineární rezoluce
-•  Definite (uspořádané) klauzule
M  vstupní rezoluce
M Selekční pravidlo R je funkce, která každé neprázdné klauzuli C přiřazuje nějaký z jejích literálů R(C) e C
3 při rezoluci vybírám z klauzule literal určený selekčním pravidlem
Hana Rudová, Logické programování I, 1 4. dubna 201 0
5
Rezoluce a logické programování
SLD-rezoluce
-• Lineární rezoluce se selekčním pravidlem     =   SLD-rezoluce (Selected Linear resolution for Definite clauses)
3  rezoluce
M  Selekční pravidlo
M  Lineární rezoluce
-•  Definite (uspořádané) klauzule
M  vstupní rezoluce
M Selekční pravidlo R je funkce, která každé neprázdné klauzuli C přiřazuje nějaký z jejích literálů R(C) e C
3 při rezoluci vybírám z klauzule literal určený selekčním pravidlem
-• Pokud se R neuvádí, pak se předpokládá výběr nejlevějšího literálů
M nejlevější literal vybírá i Prolog
Hana Rudová, Logické programování I, 14. dubna 2010                       5                                                              Rezoluce a logické programování
Lineární rezoluce se selekčním pravidlem
P = {{p}Ap,^q}Aq}},     G = {^q,^p}
{^q,^p}   {q} výběr             X
nejlevějšího    i^Pf    jP*
literálu
D
{^q^p}   {P} výběr              /
nejpravějšího     Í^j    j™
literálu
D
Hana Rudová, Logické programování I, 1 4. dubna 201 0
6
Rezoluce a logické programování
Lineární rezoluce se selekčním pravidlem
P = {{p}Ap,^q}Aq}},     G = {^q,^p}
{^q,^p} {q}                                         {^q^p} (pI
výběr             X                                          výběr              /
nejlevějšího    i^Pf   JPs                        nejpravějšího     i^q}   J™
literálu           '                                            literálu            ^
D                                                                   D
SLD-rezoluční vyvrácení P u {G} pomocí selekčního pravidla R je LD-rezoluční vyvrácení (Go, Co), ■ ■ ■, {Gn, Cn) takové, že G = Go, Gn+i = D a i?(Gí) je literal rezolvovaný v kroku í
Hana Rudová, Logické programování I, 1 4. dubna 201 0
6
Rezoluce a logické programování
Lineární rezoluce se selekčním pravidlem
P = {{p}Ap,^q}Aq}},     G = {^q,^p}
{^q,^p} {q}                                         {^q^p} (pI
výběr             X                                          výběr              /
nejlevějšího    i^Pf   JPs                        nejpravějšího     i^q}   J™
literálu           '                                            literálu            ^
D                                                                   D
SLD-rezoluční vyvrácení P u {G} pomocí selekčního pravidla R je LD-rezoluční vyvrácení (Go, Co),..., (Gn, Cn) takové, že G = Go, Gn+i = D a i?(Gí) je literal rezolvovaný v kroku í
SLD-rezoluce - korektní, úplná
Efektivita SLD-rezoluce je závislá na
3 selekčním pravidle R
3 způsobu výběru příslušné programové klauzule pro tvorbu rezolventy 3 v Prologu se vybírá vždy klauzule, která je v programu první
Hana Rudová, Logické programování I, 14. dubna 2010                       6                                                              Rezoluce a logické programování
Príklad
t: -p,r.	(D
t: -s.	(2)
P '■ -q, v.	(3)
p : -u,w.	(4)
q.	(5)
s.	(6)
u.	(7)
-t,
Hana Rudová, Logické programování I, 1 4. dubna 201 0
SLD-strom
- Ĺ
- S.
q,v,r.        :- u,w,r.
D
(5)
(7)
- v, r.
'- w,r.
fail
fail
7
Rezoluce a logické programování
Strom výpočtu (SLD-strom)
-• SLD-strom je strom tvořený všemi možnými výpočetními posloupnostmi logického programu P vzhledem k cíli G
Hana Rudová, Logické programování I, 14. dubna 2010                       8                                                              Rezoluce a logické programování
Strom výpočtu (SLD-strom)
-• SLD-strom je strom tvořený všemi možnými výpočetními posloupnostmi logického programu P vzhledem k cíli G
-• kořeny stromy jsou programové klauzule a cílová klauzule G
-• v uzlech jsou rezolventy
-• výchozím kořenem rezoluce je cílová klauzule G
Hana Rudová, Logické programování I, 1 4. dubna 201 0
8
Rezoluce a logické programování
Strom výpočtu (SLD-strom)
-• SLD-strom je strom tvořený všemi možnými výpočetními posloupnostmi logického programu P vzhledem k cíli G
M kořeny stromy jsou programové klauzule a cílová klauzule G
M v uzlech jsou rezolventy
-• výchozím kořenem rezoluce je cílová klauzule G
-• listy jsou dvojího druhu:
-• označené prázdnou klauzulí -jedná se o úspěšné uzly (succes nodes)
3 označené neprázdnou klauzulí -jedná se o neúspěšné uzly (failure nodes)
Hana Rudová, Logické programování I, 1 4. dubna 201 0
8
Rezoluce a logické programování
Strom výpočtu (SLD-strom)
-• SLD-strom je strom tvorený všemi možnými výpočetními posloupnostmi logického programu P vzhledem k cíli G
M kořeny stromy jsou programové klauzule a cílová klauzule G
M v uzlech jsou rezolventy
-• výchozím kořenem rezoluce je cílová klauzule G
-• listy jsou dvojího druhu:
-• označené prázdnou klauzulí -jedná se o úspěšné uzly (succes nodes)
3 označené neprázdnou klauzulí -jedná se o neúspěšné uzly (failure nodes)
M úplnost SLD-rezoluce zaručuje existenci cesty od kořene k úspěšnému uzlu pro každý možný výsledek příslušející cíli G
Hana Rudová, Logické programování I, 1 4. dubna 201 0
8
Rezoluce a logické programování
Príklad: SLD-strom
: -a(Z).
a(X):-b(X,Y),c(Y).           (1)
a(X) : -c(X).                        (2)
M2,3).                                  (3)
M1.2).                                  (4)
c(2).                                      (5)
Hana Rudová, Logické programování I, 1 4. dubna 201 0
a výsledná substituce
- a(Z).
:-b(Z,Y), c(Y). [Z/2.Y/3] (2,)/ \4) [Z/1,Y/2]
- cfZJ.
(5) [Z/2]
- c<3).	• •	- cf2j.	D
		(5)	[Z/2]
ail	D rz/ii		
9
Rezoluce a logické programování
Příklad: SLD-strom a výsledná substituce
: -a(Z).
a(X) : -b(X,Y),c(Y).	(1)
a(X) : -c(X).	(2)
M2,3).	(3)
M1.2).	(4)
c(2).	(5)
Cvičení:
p(B):-q(A,B),r(B)
p (A) : -q(A,A).
q(a,a).
q(a,b).
r(b).
- a(Z).
:-b(Z,Y),c(Y). [Z/2.Y/3] (3)/ \(4) [Z/1 ,Y/2]
- crz;.
(5) [Z/2]
- c<3).	• •	- cf2j.	D
		(5)	[Z/2]
ail	D ľZ/11		
ve výsledné substituci jsou pouze proměnné z dotazu, tj výsledné substituce jsou [Z/l] a [Z/2] nezajímá mě substituce [Y/2]
Hana Rudová, Logické programování I, 1 4. dubna 201 0
9
Rezoluce a logické programování
Výsledná substituce (answer substitution)
q(a). p(a,b).
:-q(X),p(X,Y). X=a, Y=b
- q(X), p(X,Y).        q(a).
[X/a]
:-p(a,Y).    P(a,b).         [Y/b]
D
[X/a, Y/b]
Hana Rudová, Logické programování I, 1 4. dubna 201 0
10
Rezoluce a logické programování
Výsledná substituce (answer substitution)
q(a). p(a,b).
:-q(X),p(X,Y). X=a, Y=b
- q(X), p(X,Y).        q(a).
[X/a]
:-p(a,Y).    P(a,b).         [Y/b]
D
[X/a, Y/b]
Každý krok SLD-rezoluce vytváří novou unifikační substituci 0t => potenciální instanciace proměnné ve vstupní cílové klauzuli
Výsledná substituce {answer substitution)
0  =   0Q01   •   •   •  0
n
složení unifikací
Hana Rudová, Logické programování I, 1 4. dubna 201 0
10
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 -"G2(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, 1 4. dubna 201 0
1 1
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 -"G2(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 h- -G
(3)Ph(BÍ)(G!(Í)A---AGn(Í))
Hana Rudová, Logické programování I, 1 4. dubna 201 0
1 1
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 M Dokazujeme nesplnitelnost
(1)  P A (VX)(--Gi(X) v -"G2(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 h -G (3)Ph(3X)(Gi(X)A---AGn(X))
a jedná se tak o důkaz existence vhodných objektů, které na základě vlastností množiny P splňují konjunkci literálů v cílové klauzuli
Hana Rudová, Logické programování I, 1 4. dubna 201 0
1 1
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 M Dokazujeme nesplnitelnost
(1)  P A (VX)(--Gi(X) v ^G2{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 h -G (3)Ph(3X)(Gi(X)A---AGn(X))
a jedná se tak o důkaz existence vhodných objektů, které na základě vlastností množiny P splňují konjunkci literálů v cílové klauzuli
M Důkaz nesplnitelnosti P u {G} znamená nalezení protipříkladu
ten pomocí SLD-stromu konstruuje termy (odpověď) splňující konjunkci v (3)
Hana Rudová, Logické programování I, 1 4. dubna 201 0
1 1
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á, Logické programování I, 14. dubna 2010                      12                                                             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
-• Korektní výpočetní strategie = prohledávání stromu do šířky
M exponenciální paměťová náročnost M složité řídící struktury
Hana Rudová, Logické programování I, 14. dubna 2010                      12                                                             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
-• Korektní výpočetní strategie = prohledávání stromu do šířky
M exponenciální paměťová náročnost M složité řídící struktury
M Použitelná výpočetní strategie = prohledávání stromu do hloubky
M jednoduché řídící struktury (zásobník)
M lineární paměťová náročnost
-• není ale úplná: nenalezne vyvrácení i když existuje
s procházení nekonečné větve stromu výpočtu
=> na nekonečných stromech dojde k zacyklení s> nedostaneme se tak na jiné existující úspěšné uzly
Hana Rudová, Logické programování I, 14. dubna 2010                      12                                                             Rezoluce a logické programování
SLD-rezoluce v Prologu: úplnost
-• Prolog: prohledávání stromu do hloubky
=> neúplnost použité výpočetní strategie
-• Implementace SLD-rezoluce v Prologu 3 není úplná
logický program: q : -r.                  (1)
r:-q.                (2)
q.                       (3)
dotaz:                  : -q.

Hana Rudová, Logické programování I, 1 4. dubna 201 0
13
Rezoluce a logické programování
Test výskytu
-• Kontrola, zda se proměnná vyskytuje v termu, kterým ji substituujeme
3 dotaz : -a(B,B).
M logický program: a(X,f(X)).
3 vede k: [B/X], [X/f(X)]
M Unifikátor pro g(Xu ...Jn)a g(f(X0,X0),f(Xi,Xi),... ,/(Xn_i,Xn_i))
X\ = f(Xo,Xo),   X2 = f(X\,Xi),...,    Xn = f(Xn-i,Xn-i)
X2 = f(f(Xo,Xo),f(Xo,Xo)), ■ ■ ■
délka termu pro Xk exponenciálně narůstá
Hana Rudová, Logické programování I, 1 4. dubna 201 0
14
Rezoluce a logické programování
Test výskytu
-• Kontrola, zda se proměnná vyskytuje v termu, kterým ji substituujeme
3 dotaz : -a(B,B).
M logický program: a(X,f(X)).
3 vede k: [B/X], [X/f(X)]
M Unifikátor pro g(Xu ...Jn)a g(f(X0,X0),f(Xi,Xi),... ,/(Xn-i,*n-i))
X\ = f(Xo,Xo),   X2 = f(X\,Xi),...,    Xn = f(Xn-i,Xn-i)
X2 = f(f(Xo,Xo),f(Xo,Xo)), ■ ■ ■
délka termu pro X^ exponenciálně narůstá => exponenciální složitost na ověření kontroly výskytu M Test výskytu se při unifikaci v Prologu neprovádí
3 Důsledek:        ?-X = f(X) uspěje s X = f (f (f (f (f (f (f (f (f (f U))))))))))
Hana Rudová, Logické programování I, 1 4. dubna 201 0
14
Rezoluce a logické programování
SLD-rezoluce v Prologu: korektnost
M Implementace SLD-rezoluce v Prologu nepoužívá při unifikaci test výskytu
=> není korektní
(1) t(X) : -p(X,X).     : -t(X).
p(Xj(X)).            X = /(/(/(/(...))))))))))        problém se projeví
Hana Rudová, Logické programování I, 1 4. dubna 201 0
15
Rezoluce a logické programování
SLD-rezoluce v Prologu: korektnost
M Implementace SLD-rezoluce v Prologu nepoužívá při unifikaci test výskytu => není korektní
(1)  t(X) : -p(X,X).     : -t(X).
p(Xj(X)).            X = /(/(/(/(...))))))))))        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, 14. dubna 2010                      15                                                             Rezoluce a logické programování
SLD-rezoluce v Prologu: korektnost
M Implementace SLD-rezoluce v Prologu nepoužívá při unifikaci test výskytu => není korektní
(1)  t(X) : -p(X,X).     : -t(X).
p(Xj(X)).            X = /(/(/(/(...))))))))))        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)
3 Řešení: problém typu (2) převést na problém typu (1) ?
Hana Rudová, Logické programování I, 1 4. dubna 201 0
15
Rezoluce a logické programování
SLD-rezoluce v Prologu: korektnost
M Implementace SLD-rezoluce v Prologu nepoužívá při unifikaci test výskytu => není korektní
(1)  t(X) : -p(X,X).     : -t(X).
p(Xj(X)).            X = /(/(/(/(...))))))))))        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)
3 Řešení: problém typu (2) převést na problém typu (1) ?
-• každá proměnná v hlavě klauzule se objeví i v těle, aby se vynutilo hledání unifikátoru (přidáme X = X pro každou X, která se vyskytuje pouze v hlavě) t: -p(X,X). p(X,f(X)):-X = X.
Hana Rudová, Logické programování I, 14. dubna 2010                      15                                                             Rezoluce a logické programování
SLD-rezoluce v Prologu: korektnost
M Implementace SLD-rezoluce v Prologu nepoužívá při unifikaci test výskytu => není korektní
(1)  t(X) : -p(X,X).     : -t(X).
p(Xj(X)).            X = /(/(/(/(...))))))))))        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)
3 Řešení: problém typu (2) převést na problém typu (1) ?
3 každá proměnná v hlavě klauzule se objeví i v těle, aby se vynutilo hledání unifikátoru (přidáme X = X pro každou X, která se vyskytuje pouze v hlavě) t: -p(X,X). p(X,f(X)):-X = X.
M optimalizace v kompilátoru mohou způsobit opět odpověď „yes"
Hana Rudová, Logické programování I, 14. dubna 2010                      15                                                             Rezoluce a logické programování
Řízení implementace: řez
řez se syntakticky chová jako kterýkoliv jiný literal nemá ale žádnou deklarativní sémantiku místo toho mění implementaci programu
V ■ -q,\,v-
ořezání
Hana Rudová, Logické programování I, 1 4. dubna 201 0
16
Rezoluce a logické programování
Řízení implementace: řez
řez se syntakticky chová jako kterýkoliv jiný literal nemá ale žádnou deklarativní sémantiku místo toho mění implementaci programu
P ■ -q,\,v-snažíme se splnit g
pokud uspěji
=> přeskočím řez a pokračuji jako by tam řez nebyl
pokud ale neuspěji (a tedy i při backtrackingu) a vracím se přes řez => vracím se až na rodiče : -p. a zkouším další větev
ořezání
Hana Rudová, Logické programování I, 1 4. dubna 201 0
16
Rezoluce a logické programování
Řízení implementace: řez
řez se syntakticky chová jako kterýkoliv jiný literal nemá ale žádnou deklarativní sémantiku místo toho mění implementaci programu P ■ -q,Uv. snažíme se splnit q
pokud uspěji
=> přeskočím řez a pokračuji jako by tam řez nebyl
pokud ale neuspěji (a tedy i při backtrackingu) a vracím se přes řez => vracím se až na rodiče : -p. a zkouším další větev => nezkouším tedy další možnosti, jak splnit p                                      upnutí
=> a nezkouším ani další možnosti, jak splnit q v SLD-stromu            ořezání
ořezání
Hana Rudová, Logické programování I, 1 4. dubna 201 0
16
Rezoluce a logické programování
Příklad: řez
t: -p,r.	(D
t: -s.	(2)
p : -q(X),\,v.	(3)
p : -u,w.	(4)
q(a).	(5)
q(b).	(6)
s.	(7)
u.	(8)
:- t. (1}/\(2)	
:-p,r.	
«x x	
:- q(X),!,v,r.	
a]	(5)       X
•	■ /vr
• •	(!) - v, r.
fail
Hana Rudová, Logické programování I, 1 4. dubna 201 0
17
Rezoluce a logické p
Príklad
a(X) : -b(X,Y),\,c(Y).	(D
a(X) : -c(X).	(2)
M2,3).	(3)
M1.2).	(4)
c(2).	(5)
s (X) : -a(X).	(6)
5(X) : -p(X).	(7)
p(B):-q(A,B),r(B).	(8)
p (A) : -íí(A,A).	(9)
q(a,a).	(10)
q(a,b).	(11)
r (b).	(12)
Hana Rudová, Logické programování I, 1 4. dubna 201 0
18
II
.- b(X,Y),!,c(Y). [X/2.Y/3] (3)
.- !,c(3). (rez) :- c(3).
fail
Rezoluce a logické programování
a(X) : -b(X,Y),c(Y),\.
a(X) : -c(X).
M2,3).
M1.2).
c(2).
5(A") : -a(X). s(X) : -p(A).
p(B):-q(A,B),r(B).
p (A) : -íí(A,A).
q(a,a).
q(a,b).
r(b).
Hana Rudová, Logické programování I, 14. dubn
• •	-b(X,Y),,	c(Y),L	
(3)/   \		(4) [X/1 ,Y/2]	
•	■ c(3),!.	•	(5)
fail		• •	_ / • • (rez)
		D	
		[X/11	
Rezoluce a logické programování
Operační a deklarativní sémantika
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 Ql odvodit nějakým rezolučním důkazem ze vstupní množiny P u {Q}.
Hí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, 1 4. dubna 201 0
21
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 Ql odvodit nějakým rezolučním důkazem ze vstupní množiny P u {Q}.
Hí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                                                 11
Hana Rudová, Logické programování I, 1 4. dubna 201 0
21
Sémantiky
Opakování: interpretace
M Interpretace 1 jazyka L je dána univerzem V a zobrazením, které přiřadí konstantě c prvek D, funkčnímu symbolu f/n n-ární operaci v V 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 li: D = Z, a := 1, b := -l,f:= " + "
Hana Rudová, Logické programování I, 1 4. dubna 201 0
22
Sémantiky
Opakování: interpretace
M Interpretace 1 jazyka L je dána univerzem V a zobrazením, které přiřadí konstantě c prvek D, funkčnímu symbolu f/n n-ární operaci v V a predikátovému symbolu p/nn-ávn\ relaci.
* příklad: F = {{f(a,b) = f(b,a)}, {f(f(a,a),b) = a}} interpretace li: D = Z, a := 1, b := -l,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, 1 4. dubna 201 0
22
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
M při zkoumání pravdivosti není nutné uvažovat modely nad všemi interpretacemi
Hana Rudová, Logické programování I, 14. dubna 2010                      23                                                                                                     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
M 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
3 Herbrandova interpretace: libovolná interpretace, která přiřazuje
M proměnným prvky Herbrandova univerza M konstantám sebe samé
M funkčním symbolům funkce, které symbolu f pro argumenty ti, ■ ■ ■ , tn přiřadí term
f(ti, • • • ,tn) M predikátovým symbolům libovolnou funkci z Herbrand. univerza do pravdivostních hodnot
Hana Rudová, Logické programování I, 1 4. dubna 201 0
23
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
M 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
3 Herbrandova interpretace: libovolná interpretace, která přiřazuje
M proměnným prvky Herbrandova univerza M konstantám sebe samé
M funkčním symbolům funkce, které symbolu f pro argumenty ti, ■ ■ ■ , tn přiřadí term
f(ti, • • • ,tn) M predikátovým symbolům libovolnou funkci z Herbrand. univerza do pravdivostních hodnot
-• Herbrandův model množiny uzavřených formulí T\
Herbrandova interpretace taková, že každá formule z T je v ní pravdivá.
Hana Rudová, Logické programování I, 14. dubna 2010                      23                                                                                                     Sémantiky
Specifikace Herbrandova modelu
-• Herbrandovy interpretace mají předdefinovaný význam funktorů a konstant
M Pro specifikaci Herbrandovy interpretace tedy stačí zadat relace pro každý predikátový symbol
Hana Rudová, Logické programování I, 1 4. dubna 201 0
24
Sémantiky
Specifikace Herbrandova modelu
-• Herbrandovy interpretace mají předdefinovaný význam funktorů a konstant
M Pro specifikaci Herbrandovy interpretace tedy stačí zadat relace pro každý predikátový symbol
-• Příklad: Herbrandova interpretace a Herbranduv model množiny formulí
lichy(s(0)).                                   % (1)
lichy(s(s(X)))   :-  lichy(X).   %  (2)
Hana Rudová, Logické programování I, 1 4. dubna 201 0
24
Sémantiky
Specifikace Herbrandova modelu
-• Herbrandovy interpretace mají předdefinovaný význam funktorů a konstant
M Pro specifikaci Herbrandovy interpretace tedy stačí zadat relace pro každý predikátový symbol
-• Příklad: Herbrandova interpretace a Herbranduv model množiny formulí
lichy(s(0)).                                   % (1)
lichy(s(s(X)))   :-  lichy(X).   %  (2)
3 li = 0                                                                                              není model (1)
Hana Rudová, Logické programování I, 1 4. dubna 201 0
24
Sémantiky
Specifikace Herbrandova modelu
-• Herbrandovy interpretace mají předdefinovaný význam funktorů a konstant
M Pro specifikaci Herbrandovy interpretace tedy stačí zadat relace pro každý predikátový symbol
-• Příklad: Herbrandova interpretace a Herbranduv model množiny formulí
lichy(s(0)).                                   % (1)
lichy(s(s(X)))   :-  lichy(X).   %  (2)
3 li = 0                                                                                              není model (1)
3 12 = {líchy(s(0))}                                                                není model (2)
Hana Rudová, Logické programování I, 1 4. dubna 201 0
24
Sémantiky
Specifikace Herbrandova modelu
-• Herbrandovy interpretace mají předdefinovaný význam funktorů a konstant
M Pro specifikaci Herbrandovy interpretace tedy stačí zadat relace pro každý predikátový symbol
-• Příklad: Herbrandova interpretace a Herbranduv model množiny formulí
lichy(s(0)).                                   % (1)
lichy(s(s(X)))   :-  lichy(X).   %  (2)
3 li = 0                                                                                              není model (1)
3 12 = {líchy(s(0))}                                                                není model (2)
M 13 = {líchy(5(0)), líchy(5(5(5(0))))}                                         není model (2)
Hana Rudová, Logické programování I, 1 4. dubna 201 0
24
Sémantiky
Specifikace Herbrandova modelu
-• Herbrandovy interpretace mají předdefinovaný význam funktorů a konstant
M Pro specifikaci Herbrandovy interpretace tedy stačí zadat relace pro každý predikátový symbol
-• Příklad: Herbrandova interpretace a Herbranduv model množiny formulí
lichy(s(0)).                                   % (1)
lichy(s(s(X)))   :-  lichy(X).   %  (2)
3 li = 0                                                                                              není model (1)
3 12 = {líchy(s(0))}                                                                         není model (2)
M 13 = {líchy(5(0)), líchy(5(5(5(0))))}                                         není model (2)
M % = {líchy(sn(0))\ne {1,3,5,7,...}}                   Herbranduv model (1) i (2)
Hana Rudová, Logické programování I, 1 4. dubna 201 0
24
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 Herbranduv model množiny formulí
lichy(s(0)).                                   % (1)
lichy(s(s(X)))   :-  lichy(X).   %  (2)
li = 0
12  = {líchy(s(0))}
13  = {líchy(5(0)), líchy(5(5(5(0))))}
14  = {líchy(sn(0))\ne {1,3,5,7,...}}
15  = {líchy(sn(0))\nGN}}
není model (1)
není model (2)
není model (2)
Herbranduv model (1) i (2)
Herbranduv model (1) i (2)
Hana Rudová, Logické programování I, 1 4. dubna 201 0
24
Sémantiky
Příklad: Herbrandovy interpretace
rodič(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, 1 4. dubna 201 0
25
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).
li = {rodíc(a,b),rodíc(b,c),predek(a,b),predek(b,c),predek(a,c li = {rodíc(a,b),rodíc(b,c),
predek(a, b), predek(b, c), predek(a, c), predek(a, a)}
li i ^2 jsou Herbrandovy modely klauzulí
Hana Rudová, Logické programování I, 1 4. dubna 201 0
25
Deklarativní a operační sémantika
M 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 Herbranduv model množiny S.
M Důsledek:
Existuje nejmenší Herbranduv model množiny S, který značíme M(S).
Hana Rudová, Logické programování I, 1 4. dubna 201 0
26
Sémantiky
Deklarativní a operační sémantika
M 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 Herbranduv model množiny S.
M Důsledek:
Existuje nejmenší Herbranduv model množiny S, který značíme M(S).
-• Deklarativní sémantikou logického programu P rozumíme jeho minimální Herbranduv model M(P).
Hana Rudová, Logické programování I, 1 4. dubna 201 0
26
Sémantiky
Deklarativní a operační sémantika
M 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 Herbranduv model množiny S.
M Důsledek:
Existuje nejmenší Herbranduv model množiny S, který značíme M(S).
-• Deklarativní sémantikou logického programu P rozumíme jeho minimální Herbranduv 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 Ql odvodit nějakým rezolučním důkazem ze vstupní množiny P u {Q}.
Hí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, 1 4. dubna 201 0
26
Sémantiky
Deklarativní a operační sémantika
M 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 Herbranduv model množiny S.
M Důsledek:
Existuje nejmenší Herbranduv model množiny S, který značíme M(S).
-• Deklarativní sémantikou logického programu P rozumíme jeho minimální Herbranduv 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 Ql odvodit nějakým rezolučním důkazem ze vstupní množiny P u {Q}.
Hí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, 1 4. dubna 201 0
26
Sémantiky