Příklad: SLD-strom a výsledná substituce
Rezoluce a logické programování (pokračování)
(1)
(2)
(3)
(4)
(5)
: -a(Z).
a(X) : -b(X,Y),c(Y). a(X) : -c(X). b(2,3). b(l,2). c(2).
Cvičení:
p(E) : -q(A,E),r(E). p(A) : -q(A,A). q(a, a). q(a, b). r(b).
Hana Rudová, Logické programování 1,11. dubna 201 2
:- 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).
- c(2). (5)
□ [Z/2]
fail
□
ÍZ/11
ve výsledné substituci jsou pouze proměnné z dotazu výsledné substituce jsou [Z/l] a [Z/2] nezajímá mě substituce [Y12]
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]
:-piajy^pi^b). [Y/b] \/
□ [X/a, Y/b]
Každý krok SLD-rezoluce vytváří novou unifikační substituci 0í => potenciální instanciace proměnné ve vstupní cílové klauzuli
Výsledná substituce (answer substitution)
9 = 0n0i ■ ■ ■ 9n složení unifikací
Význam SLD-rezolučního vyvrácení P u {G}
Množina P programových klauzulí, cílová klauzule G
Dokazujeme nesplnitelnost
(DPA(VÍ)hGi(I) v ^G2(X) v ■ ■ ■ v -.G„(*))
kde G = {^Gi, -1G2, ■ ■ ■ , ^Gn} a X je vektor proměnných v G nesplnitelnost (1) je ekvivalentní tvrzení (2) a (3)
(2) P h -G
(3) Pr-(3Í)(Gi(í)A---AG„(í))
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
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í 1,11. dubna 201 2
Rezoluce a logické programování
Hana Rudová, Logické programování 1,11. dubna 201 2
Rezoluce a logické programování
Výpočetní strategie
SLD-rezoluce v Prologu: úplnost
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
■ exponenciální paměťová náročnost
■ složité řídící struktury
Použitelná výpočetní strategie = prohledávání stromu do hloubky
■ jednoduché řídící struktury (zásobník)
■ lineární paměťová náročnost
■ není ale úplná: nenalezne vyvrácení i když existuje
■ procházení nekonečné větve stromu výpočtu
=> na nekonečných stromech dojde k zacyklení
■ nedostaneme se tak najiné existující úspěšné uzly
Hana Rudová, Logické programování 1,11. dubna 201 2
Rezoluce a logické programování
Test výskytu
Kontrola, zda se proměnná vyskytuje v termu, kterým ji substituujeme
■ dotaz : -a(B,B).
■ logický program: a(X,f(X)).
■ by vedl k: [B/X], [X/f(X)]
Unifikátorpro0(*i,...,*n) ag(f(X0,X0),f(X1,X1),...,f(Xn-1,Xn-1))
Xi=f(Xo,Xo),   Xz = f(Xi,X\),...,   Xn = f(Xn-i,Xn-i) X2=f(f(X0,Xo),f(X0,Xo)),...
délka termu pro Xt exponenciálně narůstá
=> exponenciální složitost na ověření kontroly výskytu
Test výskytu se při unifikaci v Prologu neprovádí
Důsledek:      ? - X = f(X) uspěje s X = /(/(/(/(/(/(/(/(/(/(...))))))))))
Hana Rudová, Logické programování 1,11. dubna 201 2
Rezoluce a logické programování
Prolog: prohledávání stromu do hloubky => neúplnost použité výpočetní strategie
Implementace SLD-rezoluce v Prologu ■ není úplná
logický program: q : -r. (1) r:-q. (2) q. (3)
dotaz: : -q.
q.
(3)
□
Hana Rudová, Logické programování 1,11. dubna 201 2
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). P(XJ(X)).
(2) t:-p(X,X). P(XJ(X)).
:-t(X).
X = /(/(/(/(...))))))))))      problém se projeví
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á 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ě) ř : -p(X,X).
P(XJ(X)):-X = X.
■ optimalizace v kompilátoru mohou způsobit opět odpověď „yes"
Hana Rudová, Logické programování 1,11. dubna 201 2
Rezoluce a logické programování
Řízení implementace: řez
Příklad: řez
orezaní
■ nemá ale žádnou deklarativní sémantiku
■ místo toho mění implementaci programu
■ p : -q,!, v.
S ře^le^ňfeKÍíÚV^hová jako kterýkoliv jiný literál
■ 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í
Hana Rudová, Logické programování 1,11. dubna 2012
Rezoluce a logické programování
Příklad: řez II
a(X):-b(X,Y),\,c(Y). (1)
a(X) : -c(X). (2)
fc(2,3). (3)
b(l,2). (4)
c(2). (5)
s(X) : -a(X). (6)
s(X):-p(X). (7)
p(B) : -q(A,B),r(B). (8)
p(A) :-q(A,A). (9)
q(a,a). (10)
q(a,b). (11)
r(b). (12)
Hana Rudová, Logické programování 1,11. dubna 201 2
[X/2.Y/3] (3).
(1)
b(X,Y),!,c(Y).
V
>,c(3).
(rez)
c(3).
fail
Rezoluce a logické programování
ř : -p, r. t: -s.
p : -q(X),\,v.
p : -u, w.
q(a).
q(b).
s.
u.
(D
(2)
(3)
(4)
(5)
(6)
(7)
(8)
[X/a]
:-p,r. :-s.
Y X X'
q(X),!,r,r. D
(5) "\
!,v,r.
(!) v, r.
fail
Hana Rudova, Logické programování I, 1 1. dubna 201 2
Rezoluce a logické programování
Příklad: řez
a(X) : -b(X,Y),c(Y),\.
a(X) : -c(X).
fc(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).
(1)
(2)
(3)
(4)
(5)
(6)
(7)
(8)
(9)
(10)
(11)
(12)
' s(X).
[X/2.Y/3] (3)
Hana Rudová, Logické programování 1,11. dubna 201 2
Rezoluce a logické programování
Operační sémantika
Operační a deklarativní sémantika
Operační sémantikou logického programu P rozumíme množinu 0{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 u {Cj}.
^í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 111
Opakování: interpretace
Interpretace 1 jazyka £ je dána univerzem T> a zobrazením, které přiřadí konstantě c prvek T>, funkčnímu symbolu f In n-ární operaci v D a predikátovému symbolu pln n-ární relaci.
■ příklad: F = {{f (a, b) = f (b,a)}, {f (f (a, a), b) = a}} interpretace 'h: D = Z, a := 1, b := -1,/ := " + "
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í 1,11. dubna 201 2
Hana Rudová, Logické programování 1,11. dubna 2012 14 Sémantiky
Herbrandovy interpretace
1 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
1 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
1 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 ti, ■ ■ ■ , tn přiřadí term f(ti, ■■■ ,tn)
■ predikátovým symbolům libovolnou funkci z Herbrand. univerza do pravdivostních hodnot
1 Herbrandův model množiny uzavřených formulí T: Herbrandova interpretace taková, že každá formule z P je v ní pravdivá.
Hana Rudová, Logické programování 1,11. dubna 201 2
Specifikace Herbrandova modelu
Příklad: Herbrandovy interpretace
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)). lichy(s(s(X)))
■ 2i = 0
% (D
"lichy(X). % (2)
12 = {Uchy\s(0))}
% = {líchy (5(0)), líchy (5(5(5(0))))}
24 = {líchy(sn(0))\n e {1,3,5,7,...}}
25 = {líchy(sn(0))\n e N}}
není model (1) není model (2) není model (2) Herbrandův model (1) i (2) Herbrandův model (1) i (2)
Hana Rudová, Logické programování I, 11. dubna 2012 17 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).
Připomenutí: 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 u {Cj}. ^í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í 1,11. dubna 201 2
rodic(a,b). rodi c(b,c). predek(X,Y) predek(X,Z)
rodic(X,Y).
rodic(X,Y), predek(Y,Z),
1\ = {rodíc(a, b),rodíc(b, c), predek(a, h), predek(b, c), predek(a, c)} ?2 = {rodíc(a,b),rodíc(b,c),
predek(a, b), predekib, c), predekia, c), predekia, a)}
1\ i ?2 jsou Herbrandovy modely klauzulí
Cvičení: Napište minimální Herbrandův model pro následující logický program.
muz(petr). muz(pavel). zena(olga). zena(jitka). pary(X,Y)  :- zena(X), muz(Y).
Uveďte další model tohoto programu, který není minimální.
Hana Rudová, Logické programování 1,11. dubna 2012 18 Sémantiky