Rezoluce a logické programování (pokračování)
Uspořádané klauzule II.
Uspořádané klauzule
{->Ap, ..., ~>An}_{B, -i_Bq, ..., -^Bm}_
^o,..., -lAi-i, -iBqP, ■ ■ ■, -'Bmp, -lAf+i,..., -^An}a
Hornovy klauzule
_: -Ap,... ,An._B : -B0,... ,Bm._
: - (A0, ...,Ai-i,B0p,..., Bmp,Ai+i, ...,An)a.
Příklad:
i->s(X), -.t(l), --u(X)}      {ř(Z), ->q(Z,X), --r(3)} {-.í(A-),-.q(l,A),-.r(3),-.u(A-)}
: -s(X),t(l),u(X).      t(Z) : -q(Z,X),r(3). : -s(X),q(l,A),r(3),u(X).
p = [X/A]      o- = [Z/l]
Hana Rudová, Logické programování I, 14. dubna 2010
Rezoluce a logické programování
Uspořádané klauzule (definite clauses)
Klauzule = množina literálů
Uspořádaná klauzule (definite clause) = posloupnost literálů
■ nelze volně měnit pořadí literálů
Rezoluční princip pro uspořádané klauzule:
{->Aq, ...,->An} {B, -"Bo, ■ ■ ■ i nSml
-iAí-i, -iBop,-^Bmp, -lAf+i,..., ^An}a
■ uspořádaná rezolventa: {-<Ao....."vlí-i, -<Bop.....~^Bmp, ->Aí+i.....->An}cT
■ p je přejmenování proměnných takové, že klauzule {Aq.....An\ a {B,Bq.....Bm}p nemají
společné proměnné
■ <jje nejobecnější unifikátor pro A; aBp
■ rezoluce je realizována na literálech -iAict aBpcr
■ je dodržováno pořadí literálů, tj.
{-'Bop.....-iBmp}cr jde do uspořádané rezolventy přesně na pozici -iAict
Hana Rudová, Logické programování I, 14. dubna 2010
Rezoluce a logické programován
LD-rezoluce
LD-rezoluční vyvrácení množiny uspořádaných klauzulí P u {G} je posloupnost <Go, Co),     (Gn, Cn) taková, že
■ Gí,Cí jsou uspořádané klauzule
■ G = Go
■ Gn+1 = □
■ d je uspořádaná cílová klauzule
■ Qje přejmenování klauzule z P
■ Q neobsahuje proměnné, které jsou v Gj,j < í nebo v Q, k < í
■ Gí+i,0 < i < n je uspořádaná rezolventa Gi a Q LD-rezoluce: korektní a úplná
Hana Rudová, Logické programování I, 14. dubna 2010
Rezoluce a logické programován
SLD-rezoluce
Lineární rezoluce se selekčním pravidlem   = SLD-rezoluce (Selected Linear resolution for Definite clauses)
■ rezoluce
■ Selekční pravidlo
■ Lineární rezoluce
■ Definite (uspořádané) klauzule
■ vstupní rezoluce
Selekční pravidlo R je funkce, která každé neprázdné klauzuli C přiřazuje nějaký z jejích literálů i? (C) e C
■ při rezoluci vybírám z klauzule literál určený selekčním pravidlem
Pokud se R neuvádí, pak se předpokládá výběr nejlevějšího literálu
nejlevější literál vybírá i Prolog
Hana Rudová, Logické programování I, 14. dubna 2010
Rezoluce a logické programování
Příklad: SLD-strom
ř : -p,r.
t: -s.
P '■ -q, v.
p : -u, w.
q.
s.
u.
(1)
(2)
(3)
(4)
(5)
(6)
(7)
fail
fail
Lineární rezoluce se selekčním pravidlem
P = {{p},{p,^q}Aq}}, G={^q,^p} {^q,^p} Iq}
výběr      j /
nejlevějšího   (->Pl 'P>
I /
literálu      I /
□
f^q,->pj (Pí výběr      j /
nejpravějšího   (^ll >1j
literálu       I Z
□
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 = Gq, Gn+\ = □ a R(Gí) je literál rezolvovaný v kroku i
SLD-rezoluce - korektní, úplná
Efektivita SLD-rezoluce je závislá na
■ selekčním pravidle R
■ způsobu výběru příslušné programové klauzule pro tvorbu rezolventy ■ v Prologu se vybírá vždy klauzule, která je v programu první
Hana Rudová, Logické programování I, 14. dubna 2010
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 stromyjsou programové klauzule a cílová klauzule G
v uzlech jsou rezolventy
výchozím kořenem rezoluce je cílová klauzule G listyjsou dvojího druhu:
■ označené prázdnou klauzulí - jedná se o úspěšné uzly (succes nodes)
■ označené neprázdnou klauzulí - jedná se o neúspěšné uzly (failure nodes)
ú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, 14. dubna 2010 7 Rezoluce a logické programování Hana Rudová, Logické programování I, 14. dubna 2010 8 Rezoluce a logické programování
Príklad: SLD-strom a výsledná substituce
Výsledná substituce (answer substitution)
: -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,E),r(E). p (A) : -q(A,A). q(a, a). q(a, b), r (b).
a(Z).
(1)
\(2)
(D
(2)
(3)
(4)
(5)
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)
n
[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]
q(a). p(a,b).
.-q(X), p(X,Y). X=a, Y=b
q(X),p(XJ).      q(a). [X/a] :-píaJl^a.b). [Y/b] □ [X/a,Y/b]
Každý krok SLD-rezoluce vytváří novou unifikační substituci 9i => potenciální instanciace proměnné ve vstupní cílové klauzuli
Výsledná substituce (answer substitution)
9 = 0n0i ■ ■ ■ 9„ složení unifikací
Hana Rudová, Logické programování I, 14. dubna 2010
Rezoluce a logické programování
Hana Rudová, Logické programování I, 14. dubna 2010
Rezoluce a logické programování
Význam SLD-rezolučního vyvrácení P u {G}
■ Množina P programových klauzulí, cílová klauzule G
■ Dokazujeme nesplnitelnost
(1) P a (VX)^Gi(X) 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) Ph(3Í)(Gi(Í)A---AGn(í))
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í I,14.dubna2010 11 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
■ 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 na jiné existující úspěšné uzly
Hana Rudová, Logické programování I,14.dubna2010 12 Rezoluce a logické programování
SLD-rezoluce v Prologu: úplnost
Test výskytu
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.
7 q.
(3)
□
Hana Rudová, Logické programování I, 14. dubna 2010
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í I, 14. dubna 2010
Rezoluce a logické programování
Kontrola, zda se proměnná vyskytuje v termu, kterým ji substituujeme
■ dotaz : -a(B,B).
■ logický program: a(X,f(X)).
■ vede k: [B/X], [X/f(X)]
Unifikátor pro g(Xu ... ,Xn) a 0(/(*o,*o),/(*i,*i), ■ ■ ■ ,/(*„-i,*„-i))
Xi=f(Xo,Xo),   X2 = f(X\,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í I, 14. dubna 201 0
Rezoluce a logické programování
Řízení implementace: řez
nemá ale žádnou deklarativní sémantiku místo toho mění implementaci programu
p : -q,!, v.
ko 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í I, 14. dubna 2010
Rezoluce a logické programování
Príklad: řez
Příklad: řez II
t ■ -p, y. t: -s.
p : -q(X),\,v.
p : -u, w.
q(a).
q(b).
s.
u.
(D
(2)
(3)
(4)
(5)
(6)
(7)
(8)
[y \(2)
-p,r-
[X/a]
q(X),!,v,r. D
(5) "\
!,v,r.
(!) v, r.
fail
Hana Rudová, Logické programování I, 14. dubna 2010
Rezoluce a logické programování
Příklad: řez
a(X) : -b(X,Y),c(Y),\.
a(X) : -c(X).
b(2,3).
fo(l,2).
c(2).
s(X) : -a(X). s(X) : -p(X).
p(B) : -q(A,B), y(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)
[X/2.Y/3] (3)
Hana Rudová, Logické programování I, 14. dubna 2010
Rezoluce a logické programování
a(X) : -b(X,Y),\,c(Y).
a(X) : -c(X).
fo(2,3).
fo(l,2).
c(2).
(1)
(2)
(3)
(4)
(5)
(6)
(7)
(8)
(9)
(10)
(11)
r(b). (12)
Hana Rudová, Logické programování I, 14. dubna 2010
s(X) s(X)
-a(X). -P(X).
p(B) : -q(A,B),y(B). p (A) : -q(A,A). q(a, a). q(a, b).
[X/2.Y/3] (3)
(rez)
!,c(3).
c(3).
fail
Rezoluce a logické programování
Operační a deklarativní sémantika
Operační sémantika
Opakování: interpretace
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 {g}.
^í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 ??
■ Interpretace 2 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: T> = Z,a := l,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í I, 14. dubna 2010 21 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 ti, ■ ■ ■ , tn přiřadí term
f(tl, ■■■ ,tn)
■ 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 P je v ní pravdivá.
Hana Rudová, Logické programování I, 14. dubna 2010
Hana Rudová, Logické programování I, 14. dubna 2010 22 Sémantiky
Specifikace Herbrandova modelu
1 Herbrandovy interpretace mají předdefinovaný význam funktorů a konstant
1 Pro specifikaci Herbrandovy interpretace tedy stačí zadat relace pro každý predikátový symbol
1 Příklad: Herbrandova interpretace a Herbrandův model množiny formulí
lichy(s(0)). % (1)
lichyCs(sCX)))  :- "lichy(X). % (2)
■ 2i = 0 není model (1)
■ 22 = {líchy(s(Q))} není model (2)
■ % = {líchy(s(0)),líchy(s(s(s(0))))} není model (2)
■ 24 = {líchy(sn(Q))\n e {1,3,5,7,...}} Herbrandův model (1) i (2)
■ 25 = {líchy(sn(Q))\n e N}} Herbrandův model (1) i (2)
Hana Rudová, Logické programování I, 14. dubna 201 0
Příklad: Herbrandovy interpretace
rodič(a,b). rodi c(b,c).
predek(X,Y)  :- rodic(X,Y).
predek(X.Z)  :- rodic(X,Y), predek(Y,Z).
1\ = {rodíc(a, b),rodíc(b, c), predekia, b), predek(b, c), predek(a, c)} I2 = {rodic(a,b),rodic(b,c),
predek(a,b), predekib, c), predek(a, c), predek(a, a)}
1\ i I2 jsou Herbrandovy modely klauzulí
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 Cj1 odvodit nějakým rezolučním důkazem ze vstupní množiny P u {(g}.
'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, 14. dubna 2010 25 Sémantiky Hana Rudová, Logické programování I, 14. dubna 2010 26 Sémantiky