Rezoluce a logické programování
(pokračování)
Uspořádané klauzule (definite clauses)
& Klauzule = množina literálů
* Uspořádaná klauzule (definite clause) = posloupnost liteřálů
-i- nelze volne menit poradí literálů
Rezoluční princip přo uspořádané klauzule:
_{-Ao,-An}_[B1 -Bo,-Bm\_
3 uspořádaná řezolventa: {-A0,—Ai-\, -B0p,-Bmp,—Ai+\,-An}j
-*> p je přejmenování promenných takové, že klauzule {A0,.. .,An} a {B,B0,.. .,Bm}p nemají společné promenné
i  j je nejobecnejší unifikátor pro Ai a Bp
Hana Rudová, Logické programování I, 1. dubna 2011
2
Rezoluce a logické programování
Uspořádané klauzule (definite clauses)
& Klauzule = množina literálů
* Uspořádaná klauzule (definite clause) = posloupnost liteřálů
-i- nelze volne menit poradí literálů
Rezoluční princip přo uspořádané klauzule:
_{-Ao,-An}_[B1 -Bo,-Bm\_
{-Ao,-Ai-i, -Bop,-BmP—At+i,-An} j
3 uspořádaná řezolventa: {-A0,—Ai-\, -B0p,-Bmp,—Ai+\,-An}j
-*> p je přejmenování promenných takové, že klauzule {A0,.. .,An} a {B,B0,.. .,Bm}p nemají společné promenné
i  j je nejobecnejší unifikátor pro Ai a Bp
A řezoluceje řealizována na liteřálech -Aij a Bpj
je dodržováno poradí literálu, tj.
{-B0p,-Bmp}j jde do uspořádané řezolventy přesne na pozici -Aij
Hana Rudová, Logické programování I, 1. dubna 2011 2 Rezoluce a logické programování
Uspořádané klauzule II.
C Uspořádána klauzule Hornovy klauzule
■ —A0, • • • , An- B ■ —B0, • • • , Bm-
: — (Aq, • • • ,Ai—i,BqP, • • • ,BmP,Af+i, • • • ,An)&•
Hana Rudová, Logické programování I, 1. dubna 2011
3
Rezoluce a logické programování
Uspořádané klauzule II.
Uspořádané klauzule
Hornovy klauzule
■ ~A0, • • • , An- B ■ —B0, • • • , Bm-
Příklad
■ — (Ao.....Ai—\,Bop, • • • ,Bmp,Ai+i, • • • ,An)cr,
{-s(X),-t(1), -u(X)}      {t(Z), -q(Z,X), -r(3)}_ {-s(X), -q(1,A), -r(3),-u(X)}
■ —s^^Wu^^     t (Z) ■ —q(Z,X),r(3)
■ —s(X),q(1,A),r(3),u(X)• p = [X/A]     a = [Z/l]
Hana Rudová, Logické programování I, 1. dubna 2011 3 Rezoluce a logické programování
LD-rezoluce
-í* LD-rezoluCní vyvrácení množiny uspořádaných klauzulí P u {G} je posloupnost (Go, C0),{Gn, Cn) taková, že
a Gí,Cíjsou uspořádané klauzule
G = Go
a Gi je uspořádaná cílová klauzule a C je přejmenování klauzule z P
Q neobsahuje promenné, které jsou v Gj, j < i nebo v Ck,k < i
J» Gi+l, 0 < i < n je uspořádaná rezolventa Gi a Ci
Hana Rudová, Logické programování I, 1. dubna 2011
4
Rezoluce a logické programování
LD-rezoluce
-í* LD-rezoluCní vyvrácení množiny uspořádaných klauzulí P u {G} je posloupnost (Go, C0),{Gn, Cn) taková, že
a Gí,Cíjsou uspořádané klauzule
G = Go
a Gi je uspořádaná cílová klauzule a C je přejmenování klauzule z P
Q neobsahuje promenné, které jsou v Gj, j < i nebo v Ck,k < i
J» Gi+l, 0 < i < n je uspořádaná rezolventa Gi a Ci JS> LD-rezoluce: korektní a úplná
Hana Rudová, Logické programování I, 1. dubna 2011
4
Rezoluce a logické programování
SLD-rezoluce
* Lineární rezoluce se selekCním pravidlem   = SLD-rezoluce (Selected Linear resolution for Definite clauses)
J» rezoluce
& SelekCní pravidlo
J* Lineární rezoluce
a Definite (uspořádané) klauzule
a vstupní rezoluce
Hana Rudová, Logické programování I, 1. dubna 2011
5
Rezoluce a logické programování
SLD-rezoluce
* Lineární rezoluce se selekCním pravidlem   = SLD-rezoluce (Selected Linear resolution for Definite clauses)
J» rezoluce
& SelekCní pravidlo
Jr Lineární rezoluce
a Definite (uspořádané) klauzule
a vstupní rezoluce
-i* SelekCní pravidlo R je funkce, která každé neprázdné klauzuli C prirazuje nejaký z jejích literálu R(C) g C
-i- pri rezoluci vybírám z klauzule literál urcený selekcním pravidlem
Hana Rudová, Logické programování I, 1. dubna 2011
5
Rezoluce a logické programování
SLD-řezoluce
JS> Lineární rezoluce se selekCním pravidlem   = SLD-řezoluce (Selected Linear resolution for Definite clauses)
J» rezoluce
& SelekCní pravidlo
Jr Lineární rezoluce
a Definite (usporádané) klauzule
a vstupní rezoluce
-i* SelekCní pravidlo R je funkce, která každé neprázdné klauzuli C prirazuje nejaký z jejích literálů R(C) g C
-i- pri rezoluci vybírám z klauzule literál urcený selekcním pravidlem
& Pokud se R neuvádí, pak se predpokládá výber nejlevejšího liteřálu
nejlevejší literál vybírá i Prolog
Hana Rudová, Logické programování I, 1. dubna 2011 5 Rezoluce a logické programování
Lineární rezoluce se selekCním pravidlem
P = {{p}, {p, -q}, {q}},    G = {-q,-p}
{^q,^pj {q} {^q,^p} {p}
výber      j výber      | y/
nejlevejšího   {^P} Jp} nejpravejšího Jq}
literálu      ' / literálu       ' ^
□ □
Hana Rudová, Logické programování I, 1. dubna 2011
6
Rezoluce a logické programování
Lineární rezoluce se selekčním pravidlem
P = {{p}, {p, -q}, {q}},    G = {-q,-p}
{^q,^pj {q} {^q,^p} {p}
výběr      | y/" výběr      | /
nejlevějšího   {^P} Jp} nejpravějšího Jq}
litěrálu      I / literálu       ' ^
□ □
SLD-rezoluční vyvrácení P u {G} pomocí selekčního pravidla R je LD-rezoluční vyvrácení (Go,C0),(Gn,Cn) takové, že G = G0,Gn+\ = □ a R(Gi) je literál rezolvovaný v kroku i
Hana Rudová, Logické programování I, 1. dubna 2011
6
Rezoluce a logické programování
Lineární rezoluce se selekCním pravidlem
JS> SLD-rezoluCní vyvrácení P u {G} pomocí selekcního pravidla R je
LD-rezolucní vyvrácení (Go,Co),{Gn,Cn) takové, že G = G0,Gn+\ = □ a R(Gi) je literál rezolvovaný v kroku i
M SLD-rezoluce - korektní, úplná
-í* Efektivita SLD-rezoluce je závislá na
selekcním pravidle R & zpusobu výberu príslušné programové klauzule pro tvorbu rezolventy v Prologu se vybírá vždy klauzule, která je v programu první
n
literálu
□
Hana Rudová, Logické programování I, 1. dubna 2011
6
Rezoluce a logické programování
Príklad: SLD-strom
t: -p,r. t : -s. p : -q, v. p : - u, w
q.
s. u.
(1)
(2)
(3)
(4)
(5)
(6)
(7)
: t.
:-p,r.
(3)/ \(4)
:- s.
(5)
:- v,r.
fall
:- u,w,r.
(7)
:- w,r.
.(6) □
fall
Hana Rudová, Logické programování I, 1. dubna 2011
7
Rezoluce a logické programování
Strom výpoCtu (SLD-strom)
SLD-strom je strom tvorený všemi možnými výpocetními posloupnostmi logického programu P vzhledem k cíli G
Hana Rudová, Logické programování I, 1. dubna 2011
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
-í* koreny stromy jsou programové klauzule a cílová klauzule G
-i* v uzlech jsou rezolventy
-í* výchozím kořenem rezoluce je cílová klauzule G
Hana Rudová, Logické programování I, 1. dubna 2011
8
Rezoluce a logické programování
Strom výpočtu (SLD-strom)
SLD-strom je strom tvorený všemi možnými výpocetními posloupnostmi logického programu P vzhledem k cíli G
koreny stromy jsou programové klauzule a cílová klauzule G
v uzlech jsou rezolventy
výchozím korenem rezoluce je cílová klauzule G listy jsou dvojího druhu:
-fc oznacené prázdnou klauzulí - jedná se o úspešné uzly (succes nodes)
&> oznacené neprázdnou klauzulí - jedná se o neúspešné uzly (failure nodes)
Hana Rudová, Logické programování I, 1. dubna 2011
8
Rezoluce a logické programování
Střom výpoCtu (SLD-střom)
SLD-střom je strom tvorený všemi možnými výpocetními posloupnostmi logického programu P vzhledem k cíli G
koreny stromy jsou programové klauzule a cílová klauzule G
v uzlech jsou rezolventy
výchozím korenem rezoluce je cílová klauzule G listy jsou dvojího druhu:
-fc oznacené prázdnou klauzulí - jedná se o úspešné uzly (succes nodes)
A" oznacené neprázdnou klauzulí - jedná se o neúspešné uzly (failure nodes)
úplnost SLD-rezoluce zarucuje existenci cesty od korene k úspešnému uzlu pro každý možný výsledek príslušející cíli G
Hana Rudová, Logické programování I, 1. dubna 2011
8
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).
(1)
(2)
(3)
(4)
(5)
:- a(Z).
:- b(Z,Y), c(Y).        :- c(Z). [Z/2,Y/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, 1. dubna 2011
9
Rezoluce a logické programování
Prí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).
:- b(Z,Y), c(Y).        :- c(Z). [Z/2,Y/3] \(4) [Z/1,Y/2]       \ (5) [Z/2]
:- c(3).
fall
:- c(2). (5)
□
[Z/1]
□
[Z/2]
ve výsledné substituci jsou pouze promenné z dotazu, tj. výsledné substituce jsou [Z/l] a [Z/2] nezajímá me substituce [Y/2]
Hana Rudová, Logické programování I, 1. dubna 2011
9
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, 1. dubna 2011
10
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]
iS* 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, 1. dubna 2011
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 -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, 1. dubna 2011
11
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 v (3X)(Gi(X) A--- A Gn(X))
Hana Rudová, Logické programování I, 1. dubna 2011
11
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 v (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, 1. dubna 2011
11
Rezoluce a logické programování
Význam SLD-rezoluCní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 = {-Gl, -G2, - - - , — Gn} a X je vektor proměnných v G nesplnitelnost (1) je ekvivalentní tvrzení (2) a (3)
(2) P \--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
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, 1. dubna 2011
11
Rezoluce a logické programování
VýpoCetní strategie
Korektní výpoCetní strategie prohledávání stromu výpoctu musí zarucit, že se každý (konecný) výsledek nalézt v konecném case
Hana Rudová, Logické programování I, 1. dubna 2011
12
Rezoluce a logické programování
Výpocetní strategie
Korektní výpocetní strategie prohledávání stromu výpoctu musí zarucit, že se každý (konecný) výsledek nalézt v konecném case
& Korektní výpocetní strategie = prohledávání stromu do šírky
& exponenciální pamet'ová nárocnost a složité rídící struktury
Hana Rudová, Logické programování I, 1. dubna 2011
12
Rezoluce a logické programování
Výpočetní strategie
Korektní výpočetní strategie prohledávání stromu výpoctu musí zarucit, že se každý (konecný) výsledek nalézt v konecném case
& Korektní výpocetní strategie = prohledávání stromu do šírky
& exponenciální pamet'ová nárocnost a složité rídící struktury
JS> Použitelná výpocetní strategie = prohledávání stromu do hloubky
& jednoduché rídící struktury (zásobník) * lineární pamet'ová nárocnost
s> není ale úplná: nenalezne vyvrácení i když existuje
procházení nekonecné vetve stromu výpoctu => na nekonecných stromech dojde k zacyklení nedostaneme se tak na jiné existující úspešné uzly
Hana Rudová, Logické programování I, 1. dubna 2011 12 Rezoluce a logické programování
SLD-rezoluce v Prologu: úplnost
-í* Prolog: prohledávání stromu do hloubky
=> neúplnost použité výpocetní 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, 1. dubna 2011
13
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)). vede 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, 1. dubna 2011
14
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)). vede 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 & Test výskytu se pri unifikaci v Prologů 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, 1. dubna 2011 14 Rezoluce a logické programování
SLD-řezoluce 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, 1. dubna 2011
15
Rezoluce a logické programování
SLD-rezoluče 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, 1. dubna 2011
15
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) prevést na problém typu (1) ?
Hana Rudová, Logické programování I, 1. dubna 2011
15
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) prevé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, 1. dubna 2011
15
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) p(X,f(X)).
: -t. yes
dokazovací systém nehledá unifikátor pro X a f(X)
Rešení: problém typu (2) prevé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, 1. d bna 2011
15
Rezoluce a logické programování
Ří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, 1. dubna 2011
16
Rezoluce a logické programování
Řízení implementace: řez
rez se syntakticky chová jako kterýkoliv jiný literál nemá ale žádnou deklarativní sémantiku místo toho mení implementaci přogřamu
p ■ —q,
snažíme se splnit q
pokud uspeji
=> p reskocím rez a pokracuji jako by tam r ez 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, 1. dubna 2011
16
Rezoluce a logické programování
Rízení implementace: rez
r ez 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
=> p reskocím rez a pokracuji jako by tam r ez nebyl
:- q,!,v.
upnutí
ořezání
pokud ale neuspeji (a tedy i pri backtrackingu) a vracím se pres rez => vracím se až na rodice : -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á, Logické programování I, 1. dubna 2011
16
Rezoluce a logické programování
Príklad: rez
t: -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)
(D/ \<2)
:- p,r. :- q(X),!,v,r.
[X/a]
(5)
:- ! v r
(!) :— v, r.
fail
(7)
□
Hana Rudová, Logické programování I, 1. dubna 2011
17
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).
Příklad: řez 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, 1. dubna 2011
18
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).
Příklad: řez III
(1)
(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, 1. dubna 2011
19
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, 1. dubna 2011
21
Sémantiky
Opeřacní sémantika
Opeřacní 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}.
1tímto výrazem jsou míneny všechny cíle, pro než zmínený rezolucní dukaz existuje.
iS* Deklarativní sémantika logického programu P ???
Hana Rudová, Logické programování I, 1. dubna 2011
21
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 In 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 11: D = Z,a := 1,b := -1,f := " + "
Hana Rudová, Logické programování I, 1. dubna 2011
22
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, 1. dubna 2011
22
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* p r i zkoumání pravdivosti není nutné uvažovat modely nad všemi interpretacemi
Hana Rudová, Logické programování I, 1. dubna 2011
23
Sémantiky
Herbrandovy interpretace
Omezení na obor skládající se ze symbolických výrazů tvorených z predikátových a fůnkcních symbolů daného jazyka
i* pri zkoumání pravdivosti není nutné uvažovat modely nad všemi interpretacemi
Herbrandovo univerzům: množina všech termů bez promenných, které mohou být tvoreny funkcními symboly a konstantami daného jazyka
Herbrandova interpretace: libovolná interpretace, která prirazuje
i* promenným prvky Herbrandova univerza Jť konstantám sebe samé
J* funkcním symbolům funkce, které symbolu f pro argumenty ti, • • • ,tn priradí term
f(tl, • • • ,tn)
J* predikátovým symbolům libovolnou funkci z Herbrand. univerza do pravdivostních hodnot
Hana Rudová, Logické programování I, 1. dubna 2011
23
Sémantiky
Heřbřandovy interpretace
Omezení na obor skládající se ze symbolických výřazu tvořených z předikátových a funkčních symbolu daného jazyka
i* pri zkoumání pravdivosti není nutné uvažovat modely nad všemi interpretacemi
JS> Heřbřandovo univeřzum: 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é
& funkcním symbolum funkce, které symbolu f pro argumenty t1, • • • ,tn priradí term
f(tl, • • • ,tn)
J* predikátovým symbolum libovolnou funkci z Herbrand. univerza do pravdivostních hodnot
& Heřbřandův 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, 1. dubna 2011
23
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, 1. dubna 2011
24
Sémantiky
Specifikace Herbrandova modelu
C Herbrandovy interpretace mají p r 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 Herbranduv model množiny formulí
1ichy(s(0)). % (1)
1ichy(s(s(X))) :- lichy(X). % (2)
Hana Rudová, Logické programování I, 1. dubna 2011
24
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)
Hana Rudová, Logické programování I, 1. dubna 2011
24
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 1l = 0 není model (1)
12 = {lichy(s(0))} není model (2)
Hana Rudová, Logické programování I, 1. dubna 2011
24
Sémantiky
Specifikace Herbrandova modeIu
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(G)). % (1)
1ichy(s(s(X))) i- lichy(X). % (2)
a I1 = 0 není model (l)
a ll = {lichyisi0))} není model (Z)
Ib = {lichyis i0)), lichy is is is i0))))} není model (Z)
Hana Rudová, Logické programování I, l. dubna ZOll
Sémantiky
Spečifikače 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(G)). % (1)
1ichy(s(s(X))) i- lichy(X). % (2)
a li = 0 není model (l)
a l2 = {lichy(s(0))} není model (Z)
?3 = {lichy(s(0)), lichy(s(s(s(0))))} není model (Z)
l4 = {lichy (sn(0))\n e {i, 3, 5, V,...}} Herbrandúv model (l) i (Z)
Hana Rudová, Logické programování I, l. dubna ZOll
Sémantiky
Spečifikače Herbrandova modelu
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)
15 = {lichy(sn(0))\n e N}} Herbranduv model (1) i (2)
Hana Rudová, Logické programování I, 1. dubna 2011
24
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, 1. dubna 2011
25
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).
11 = {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)}
li i l2 jsou Herbrandovy modely klauzulí
Hana Rudová, Logické programování I, 1. dubna 2011
25
Sémantiky
a operacní sémantika
& Je-li S množina programových klauzulí a M libovolná množina Herbrandových modelu S, pak průnik techto modelů je opet Herbranduv model množiny S.
JS> Důsledek:
Existuje nejmenší Herbrandův model množiny S, který znacíme M(S).
Hana Rudová, Logické programování I, 1. dubna 2011
26
Sémantiky
a operacní sémantika
ii> Je-li S množina programových klauzulí a M libovolná množina Herbrandových modelu S, pak průnik techto modelů je opet Herbranduv 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, 1. dubna 2011
26
Sémantiky
a opeřacní sémantika
ii> Je-li S množina programových klauzulí a M libovolná množina Herbrandových modelů S, pak přůnik techto modelů je opet Herbrandův model množiny S.
JS> Důsledek:
Existuje nejmenší Heřbřandův model množiny S, který znacíme M(S).
-á* Deklařativní sémantikou logického programu P rozumíme jeho minimální Herbrandův model M(P).
& Opeřacní 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í dukaz existuje.
Hana Rudová, Logické programování I, 1. dubna 2011
26
Sémantiky
a operacní sémantika
& Je-li S množina programových klauzulí a M libovolná množina Herbrandových modelu 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).
& 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 důkazem 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.
-i* Pro libovolný logický program P platí      M(P) = O(P)
Hana Rudová, Logické programování I, 1. dubna 2011
26
Sémantiky