Rezoluce a logické programování (pokračování)
Logický program
Programová klauzule: právě jeden pozitivní literál (fakt nebo pravidlo)
Logický program: konečná množina programových klauzulí
Příklad:
logický program jako množina klauzulí:
P = {P1, P2, P3}
P1 = {p}, P2 = {p, q}, P3 = {q}
Hana Rudová, Logické programování I, 30. března 2007 2 Rezoluce a logické programování
Logický program
Programová klauzule: právě jeden pozitivní literál (fakt nebo pravidlo)
Logický program: konečná množina programových klauzulí
Příklad:
logický program jako množina klauzulí:
P = {P1, P2, P3}
P1 = {p}, P2 = {p, q}, P3 = {q}
logický program v prologovské notaci:
p.
p : -q.
q.
cílová klauzule: G = {q, p} : -q, p.
Hana Rudová, Logické programování I, 30. března 2007 2 Rezoluce a logické programování
Lineární rezoluce pro Hornovy klauzule
Začneme s cílovou klauzulí: C0 = G
Boční klauzule vybíráme z programových klauzulí P
G = {q, p} P = {P1, P2, P3} : P1 = {p}, P2 = {p, q}, P3 = {q}
: -q, p. p. p : -q, q.
Hana Rudová, Logické programování I, 30. března 2007 3 Rezoluce a logické programování
Lineární rezoluce pro Hornovy klauzule
Začneme s cílovou klauzulí: C0 = G
Boční klauzule vybíráme z programových klauzulí P
G = {q, p} P = {P1, P2, P3} : P1 = {p}, P2 = {p, q}, P3 = {q}
: -q, p. p. p : -q, q.
{ q, p}
{ p}
{q}
{p}
Hana Rudová, Logické programování I, 30. března 2007 3 Rezoluce a logické programování
Lineární rezoluce pro Hornovy klauzule
Začneme s cílovou klauzulí: C0 = G
Boční klauzule vybíráme z programových klauzulí P
G = {q, p} P = {P1, P2, P3} : P1 = {p}, P2 = {p, q}, P3 = {q}
: -q, p. p. p : -q, q.
{ q, p}
{ p}
{q}
{p}
{ q, p}
{ p} {p, q}
{q}
{ q} {q}
Hana Rudová, Logické programování I, 30. března 2007 3 Rezoluce a logické programování
Lineární rezoluce pro Hornovy klauzule
Začneme s cílovou klauzulí: C0 = G
Boční klauzule vybíráme z programových klauzulí P
G = {q, p} P = {P1, P2, P3} : P1 = {p}, P2 = {p, q}, P3 = {q}
: -q, p. p. p : -q, q.
{ q, p}
{ p}
{q}
{p}
{ q, p}
{ p} {p, q}
{q}
{ q} {q}
Střední klauzule jsou cílové klauzule
Hana Rudová, Logické programování I, 30. března 2007 3 Rezoluce a logické programování
Lineární vstupní rezoluce
Vstupní rezoluce na P  {G}
(opakování:) alespoň jedna z klauzulí použitá při rezoluci je z výchozí vstupní množiny
začneme s cílovou klauzulí: C0 = G
boční klauzule jsou vždy z P (tj. jsou to programové klauzule)
Hana Rudová, Logické programování I, 30. března 2007 4 Rezoluce a logické programování
Lineární vstupní rezoluce
Vstupní rezoluce na P  {G}
(opakování:) alespoň jedna z klauzulí použitá při rezoluci je z výchozí vstupní množiny
začneme s cílovou klauzulí: C0 = G
boční klauzule jsou vždy z P (tj. jsou to programové klauzule)
(Opakování:) Lineární rezoluční důkaz C z S je posloupnost dvojic
C0, B0 , . . . Cn, Bn taková, že C = Cn+1 a
C0 a každá Bi jsou prvky S nebo některé Cj, j < i
každá Ci+1, i  n je rezolventa Ci a Bi
Hana Rudová, Logické programování I, 30. března 2007 4 Rezoluce a logické programování
Lineární vstupní rezoluce
Vstupní rezoluce na P  {G}
(opakování:) alespoň jedna z klauzulí použitá při rezoluci je z výchozí vstupní množiny
začneme s cílovou klauzulí: C0 = G
boční klauzule jsou vždy z P (tj. jsou to programové klauzule)
(Opakování:) Lineární rezoluční důkaz C z S je posloupnost dvojic
C0, B0 , . . . Cn, Bn taková, že C = Cn+1 a
C0 a každá Bi jsou prvky S nebo některé Cj, j < i
každá Ci+1, i  n je rezolventa Ci a Bi
Lineární vstupní (Linear Input) rezoluce (LI­rezoluce) C z P  {G}
posloupnost dvojic C0, B0 , . . . Cn, Bn taková, že C = Cn+1 a
C0 = G a každá Bi jsou prvky P lineární rezoluce + vstupní rezoluce
každá Ci+1, i  n je rezolventa Ci a Bi
Hana Rudová, Logické programování I, 30. března 2007 4 Rezoluce a logické programování
Cíle a fakta při lineární rezoluci
Věta: Je-li S nesplnitelná množina Hornových klauzulí, pak S obsahuje alespoň
jeden cíl a jeden fakt.
pokud nepoužiji cíl, mám pouze fakta (1 pozit.literál) a pravidla (1 pozit.literál a alespoň
jeden negat. literál), při rezoluci mi stále zůstává alespoň jeden pozit. literál
Hana Rudová, Logické programování I, 30. března 2007 5 Rezoluce a logické programování
Cíle a fakta při lineární rezoluci
Věta: Je-li S nesplnitelná množina Hornových klauzulí, pak S obsahuje alespoň
jeden cíl a jeden fakt.
pokud nepoužiji cíl, mám pouze fakta (1 pozit.literál) a pravidla (1 pozit.literál a alespoň
jeden negat. literál), při rezoluci mi stále zůstává alespoň jeden pozit. literál
pokud nepoužiji fakt, mám pouze cíle (negat.literály) a pravidla (1 pozit.literál a alespoň
jeden negat. literál), v rezolventě mi stále zůstávají negativní literály
Hana Rudová, Logické programování I, 30. března 2007 5 Rezoluce a logické programování
Cíle a fakta při lineární rezoluci
Věta: Je-li S nesplnitelná množina Hornových klauzulí, pak S obsahuje alespoň
jeden cíl a jeden fakt.
pokud nepoužiji cíl, mám pouze fakta (1 pozit.literál) a pravidla (1 pozit.literál a alespoň
jeden negat. literál), při rezoluci mi stále zůstává alespoň jeden pozit. literál
pokud nepoužiji fakt, mám pouze cíle (negat.literály) a pravidla (1 pozit.literál a alespoň
jeden negat. literál), v rezolventě mi stále zůstávají negativní literály
Věta: Existuje-li rezoluční důkaz prázdné množiny z množiny S Hornových
klauzulí, pak tento rezoluční strom má v listech jedinou cílovou klauzuli.
pokud začnu důkaz pravidlem a faktem, pak dostanu zase pravidlo
pokud začnu důkaz dvěma pravidly, pak dostanu zase pravidlo
na dvou faktech rezolvovat nelze
Hana Rudová, Logické programování I, 30. března 2007 5 Rezoluce a logické programování
Cíle a fakta při lineární rezoluci
Věta: Je-li S nesplnitelná množina Hornových klauzulí, pak S obsahuje alespoň
jeden cíl a jeden fakt.
pokud nepoužiji cíl, mám pouze fakta (1 pozit.literál) a pravidla (1 pozit.literál a alespoň
jeden negat. literál), při rezoluci mi stále zůstává alespoň jeden pozit. literál
pokud nepoužiji fakt, mám pouze cíle (negat.literály) a pravidla (1 pozit.literál a alespoň
jeden negat. literál), v rezolventě mi stále zůstávají negativní literály
Věta: Existuje-li rezoluční důkaz prázdné množiny z množiny S Hornových
klauzulí, pak tento rezoluční strom má v listech jedinou cílovou klauzuli.
pokud začnu důkaz pravidlem a faktem, pak dostanu zase pravidlo
pokud začnu důkaz dvěma pravidly, pak dostanu zase pravidlo
na dvou faktech rezolvovat nelze
 dokud nepoužiji cíl pracuji stále s množinou faktů a pravidel
Hana Rudová, Logické programování I, 30. března 2007 5 Rezoluce a logické programování
Cíle a fakta při lineární rezoluci
Věta: Je-li S nesplnitelná množina Hornových klauzulí, pak S obsahuje alespoň
jeden cíl a jeden fakt.
pokud nepoužiji cíl, mám pouze fakta (1 pozit.literál) a pravidla (1 pozit.literál a alespoň
jeden negat. literál), při rezoluci mi stále zůstává alespoň jeden pozit. literál
pokud nepoužiji fakt, mám pouze cíle (negat.literály) a pravidla (1 pozit.literál a alespoň
jeden negat. literál), v rezolventě mi stále zůstávají negativní literály
Věta: Existuje-li rezoluční důkaz prázdné množiny z množiny S Hornových
klauzulí, pak tento rezoluční strom má v listech jedinou cílovou klauzuli.
pokud začnu důkaz pravidlem a faktem, pak dostanu zase pravidlo
pokud začnu důkaz dvěma pravidly, pak dostanu zase pravidlo
na dvou faktech rezolvovat nelze
 dokud nepoužiji cíl pracuji stále s množinou faktů a pravidel
pokud použiji v důkazu cílovou klauzulí,
fakta mi ubírají negat.literály, pravidla mi je přidávají,
v rezolventě mám stále samé negativní literály, tj. nelze rezolvovat s dalším cílem
Hana Rudová, Logické programování I, 30. března 2007 5 Rezoluce a logické programování
Korektnost a úplnost
Věta: Množina S Hornových klauzulí je nesplnitelná, právě když existuje
rezoluční vyvrácení S pomocí vstupní rezoluce.
Korektnost platí stejně jako pro ostatní omezení rezoluce
Úplnost LI­rezoluce pro Hornovy klauzule:
Necht' P je množina programových klauzulí a G cílová klauzule.
Je­li množina P  {G} Hornových klauzulí nesplnitelná,
pak existuje rezoluční vyvrácení P  {G} pomocí LI­rezoluce.
vstupní rezoluce pro (obecnou) formuli sama o sobě není úplná
= LI­rezoluce aplikovaná na (obecnou) formuli nezaručuje,
že nalezeneme důkaz, i když formule platí!
Hana Rudová, Logické programování I, 30. března 2007 6 Rezoluce a logické programování
Korektnost a úplnost
Věta: Množina S Hornových klauzulí je nesplnitelná, právě když existuje
rezoluční vyvrácení S pomocí vstupní rezoluce.
Korektnost platí stejně jako pro ostatní omezení rezoluce
Úplnost LI­rezoluce pro Hornovy klauzule:
Necht' P je množina programových klauzulí a G cílová klauzule.
Je­li množina P  {G} Hornových klauzulí nesplnitelná,
pak existuje rezoluční vyvrácení P  {G} pomocí LI­rezoluce.
vstupní rezoluce pro (obecnou) formuli sama o sobě není úplná
= LI­rezoluce aplikovaná na (obecnou) formuli nezaručuje,
že nalezeneme důkaz, i když formule platí!
Význam LI­rezoluce pro Hornovy klauzule:
P = {P1, . . . , Pn}, G = {G1, . . . , Gm}
LI­rezolucí ukážeme nesplnitelnost P1      Pn  (G1      Gm)
Hana Rudová, Logické programování I, 30. března 2007 6 Rezoluce a logické programování
Korektnost a úplnost
Věta: Množina S Hornových klauzulí je nesplnitelná, právě když existuje
rezoluční vyvrácení S pomocí vstupní rezoluce.
Korektnost platí stejně jako pro ostatní omezení rezoluce
Úplnost LI­rezoluce pro Hornovy klauzule:
Necht' P je množina programových klauzulí a G cílová klauzule.
Je­li množina P  {G} Hornových klauzulí nesplnitelná,
pak existuje rezoluční vyvrácení P  {G} pomocí LI­rezoluce.
vstupní rezoluce pro (obecnou) formuli sama o sobě není úplná
= LI­rezoluce aplikovaná na (obecnou) formuli nezaručuje,
že nalezeneme důkaz, i když formule platí!
Význam LI­rezoluce pro Hornovy klauzule:
P = {P1, . . . , Pn}, G = {G1, . . . , Gm}
LI­rezolucí ukážeme nesplnitelnost P1      Pn  (G1      Gm)
pokud tedy předpokládáme, že program {P1, . . . , Pn} platí,
tak musí být nepravdivá (G1      Gm), tj. musí platit G1      Gm
Hana Rudová, Logické programování I, 30. března 2007 6 Rezoluce a logické programování
Uspořádané klauzule (definite clauses)
Klauzule = množina literálů
Uspořádáná klauzule (definite clause) = posloupnost literálů
nelze volně měnit pořadí literálů
Rezoluční princip pro uspořádané klauzule:
{A0, . . . , An} {B, B0, . . . , Bm}
{A0, . . . , Ai-1, B0, . . . , Bm,Ai+1, . . . , An}
uspořádaná rezolventa: {A0, . . . , Ai-1, B0, . . . , Bm,Ai+1, . . . , An}
 je přejmenování proměnných takové, že klauzule {A0, . . . , An} a {B, B0, . . . , Bm} nemají
společné proměnné
 je nejobecnější unifikátor pro Ai a B
Hana Rudová, Logické programování I, 30. března 2007 7 Rezoluce a logické programování
Uspořádané klauzule (definite clauses)
Klauzule = množina literálů
Uspořádáná klauzule (definite clause) = posloupnost literálů
nelze volně měnit pořadí literálů
Rezoluční princip pro uspořádané klauzule:
{A0, . . . , An} {B, B0, . . . , Bm}
{A0, . . . , Ai-1, B0, . . . , Bm,Ai+1, . . . , An}
uspořádaná rezolventa: {A0, . . . , Ai-1, B0, . . . , Bm,Ai+1, . . . , An}
 je přejmenování proměnných takové, že klauzule {A0, . . . , An} a {B, B0, . . . , Bm} nemají
společné proměnné
 je nejobecnější unifikátor pro Ai a B
rezoluce je realizována na literálech Ai a B
je dodržováno pořadí literálů, tj.
{B0, . . . , Bm} jde do uspořádané rezolventy přesně na pozici Ai
Hana Rudová, Logické programování I, 30. března 2007 7 Rezoluce a logické programování
Uspořádané klauzule II.
Uspořádáné klauzule
{A0, . . . , An} {B, B0, . . . , Bm}
{A0, . . . , Ai-1, B0, . . . , Bm,Ai+1, . . . , An}
Hornovy klauzule
: -A0, . . . , An. B : -B0, . . . , Bm.
: -(A0, . . . , Ai-1, B0, . . . , Bm,Ai+1, . . . , An).
Hana Rudová, Logické programování I, 30. března 2007 8 Rezoluce a logické programování
Uspořádané klauzule II.
Uspořádáné klauzule
{A0, . . . , An} {B, B0, . . . , Bm}
{A0, . . . , Ai-1, B0, . . . , Bm,Ai+1, . . . , An}
Hornovy klauzule
: -A0, . . . , An. B : -B0, . . . , Bm.
: -(A0, . . . , Ai-1, B0, . . . , Bm,Ai+1, . . . , An).
Příklad:
{s(X), t(1), u(X)} {t(Z), q(Z, X), r(3)}
{s(X), q(1, A), r(3),u(X)}
: -s(X), t(1), u(X). t(Z) : -q(Z, X), r(3).
: -s(X), q(1, A), r(3),u(X).
 = [X/A]  = [Z/1]
Hana Rudová, Logické programování I, 30. března 2007 8 Rezoluce a logické programování
LD-rezoluce
LD-rezoluční vyvrácení množiny uspořádaných klauzulí P  {G} je
posloupnost G0, C0 , . . . , Gn, Cn taková, že
Gi, Ci jsou uspořádané klauzule
G = G0
Gn+1 =
Gi 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 Ck, k  i
Gi+1, 0  i  n je uspořádaná rezolventa Gi a Ci
Hana Rudová, Logické programování I, 30. března 2007 9 Rezoluce a logické programování
LD-rezoluce
LD-rezoluční vyvrácení množiny uspořádaných klauzulí P  {G} je
posloupnost G0, C0 , . . . , Gn, Cn taková, že
Gi, Ci jsou uspořádané klauzule
G = G0
Gn+1 =
Gi 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 Ck, k  i
Gi+1, 0  i  n je uspořádaná rezolventa Gi a Ci
LD-rezoluce: korektní a úplná
Hana Rudová, Logické programování I, 30. března 2007 9 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
Hana Rudová, Logické programování I, 30. března 2007 10 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ů R(C)  C
při rezoluci vybírám s klauzule literál určený selekčním pravidlem
Hana Rudová, Logické programování I, 30. března 2007 10 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ů R(C)  C
při rezoluci vybírám s 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, 30. března 2007 10 Rezoluce a logické programování
Lineární rezoluce se selekčním pravidlem
P = {{p}, {p, q}, {q}}, G = {q, p}
výběr
nejlevějšího
literálu
{ q, p}
{ p}
{q}
{p}
výběr
nejpravějšího
literálu
{ q, p}
{ q}
{p}
{q}
Hana Rudová, Logické programování I, 30. března 2007 11 Rezoluce a logické programování
Lineární rezoluce se selekčním pravidlem
P = {{p}, {p, q}, {q}}, G = {q, p}
výběr
nejlevějšího
literálu
{ q, p}
{ p}
{q}
{p}
výběr
nejpravějšího
literálu
{ q, p}
{ q}
{p}
{q}
SLD-rezoluční vyvrácení P  {G} pomocí selekčního pravidla R je
LD-rezoluční vyvrácení G0, C0 , . . . , Gn, Cn takové, že G = G0, Gn+1 = a
R(Gi) je literál rezolvovaný v kroku i
Hana Rudová, Logické programování I, 30. března 2007 11 Rezoluce a logické programování
Lineární rezoluce se selekčním pravidlem
P = {{p}, {p, q}, {q}}, G = {q, p}
výběr
nejlevějšího
literálu
{ q, p}
{ p}
{q}
{p}
výběr
nejpravějšího
literálu
{ q, p}
{ q}
{p}
{q}
SLD-rezoluční vyvrácení P  {G} pomocí selekčního pravidla R je
LD-rezoluční vyvrácení G0, C0 , . . . , Gn, Cn takové, že G = G0, Gn+1 = a
R(Gi) 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, 30. března 2007 11 Rezoluce a logické programování
Příklad: SLD-strom
fail fail
(1) (2)
(6)
(7)(5)
(3) (4)
:- q,v,r.
:- v,r. :- w,r.
:- u,w,r.
:- t.
:- s.:- p,r.
t : -p, r. (1)
t : -s. (2)
p : -q, v. (3)
p : -u, w. (4)
q. (5)
s. (6)
u. (7)
: -t.
Hana Rudová, Logické programování I, 30. března 2007 12 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, 30. března 2007 13 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, 30. března 2007 13 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
listy jsou 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)
Hana Rudová, Logické programování I, 30. března 2007 13 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
listy jsou 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, 30. března 2007 13 Rezoluce a logické programování
Příklad: SLD­strom a výsledná substituce
(1)
fail
(2)
(5)
:- c(3). :- c(2).
:- a(Z).
:- b(Z,Y), c(Y).
(4) [Z/1,Y/2][Z/2,Y/3] (3)
:- c(Z).
(5) [Z/2]
[Z/2]
[Z/1]
: -a(Z).
a(X) : -b(X, Y), c(Y). (1)
a(X) : -c(X). (2)
b(2, 3). (3)
b(1, 2). (4)
c(2). (5)
Hana Rudová, Logické programování I, 30. března 2007 14 Rezoluce a logické programování
Příklad: SLD­strom a výsledná substituce
(1)
fail
(2)
(5)
:- c(3). :- c(2).
:- a(Z).
:- b(Z,Y), c(Y).
(4) [Z/1,Y/2][Z/2,Y/3] (3)
:- c(Z).
(5) [Z/2]
[Z/2]
[Z/1]
: -a(Z).
a(X) : -b(X, Y), c(Y). (1)
a(X) : -c(X). (2)
b(2, 3). (3)
b(1, 2). (4)
c(2). (5)
Cvičení:
p(B) : -q(A, B), r(B). ve výsledné substituci jsou pouze proměnné z dotazu, tj.
p(A) : -q(A, A). výsledné substituce jsou [Z/1] a [Z/2]
q(a, a). nezajímá mě substituce [Y/2]
q(a, b).
r(b).
Hana Rudová, Logické programování I, 30. března 2007 14 Rezoluce a logické programování
Výsledná substituce (answer substitution)
:-q(X), p(X,Y).
X=a, Y=b
q(a).
p(a,b).
[Y/b]
[X/a]
[X/a,Y/b]
q(a).
p(a,b).
:- q(X), p(X,Y).
:- p(a,Y).
Hana Rudová, Logické programování I, 30. března 2007 15 Rezoluce a logické programování
Výsledná substituce (answer substitution)
:-q(X), p(X,Y).
X=a, Y=b
q(a).
p(a,b).
[Y/b]
[X/a]
[X/a,Y/b]
q(a).
p(a,b).
:- q(X), p(X,Y).
:- p(a,Y).
Každý krok SLD-rezoluce vytváří novou unifikační substituci i
 potenciální instanciace proměnné ve vstupní cílové klauzuli
Výsledná substituce (answer substitution)
 = 01    n složení unifikací
Hana Rudová, Logické programování I, 30. března 2007 15 Rezoluce a logické programování
Význam SLD-rezolučního vyvrácení P  {G}
Množina P proaramových klauzulí, cílová klauzule G
Dokazujeme nesplnitelnost
(1) P  (X)(G1(X)  G2(X)      Gn(X))
kde G = {G1, G2,    , Gn} a X je vektor proměnných v G
Hana Rudová, Logické programování I, 30. března 2007 16 Rezoluce a logické programování
Význam SLD-rezolučního vyvrácení P  {G}
Množina P proaramových klauzulí, cílová klauzule G
Dokazujeme nesplnitelnost
(1) P  (X)(G1(X)  G2(X)      Gn(X))
kde G = {G1, G2,    , Gn} a X je vektor proměnných v G
nesplnitelnost (1) je ekvivalentní tvrzení (2) a (3)
(2) P G
(3) P (X)(G1(X)      Gn(X))
Hana Rudová, Logické programování I, 30. března 2007 16 Rezoluce a logické programování
Význam SLD-rezolučního vyvrácení P  {G}
Množina P proaramových klauzulí, cílová klauzule G
Dokazujeme nesplnitelnost
(1) P  (X)(G1(X)  G2(X)      Gn(X))
kde G = {G1, G2,    , Gn} a X je vektor proměnných v G
nesplnitelnost (1) je ekvivalentní tvrzení (2) a (3)
(2) P G
(3) P (X)(G1(X)      Gn(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, 30. března 2007 16 Rezoluce a logické programování
Význam SLD-rezolučního vyvrácení P  {G}
Množina P proaramových klauzulí, cílová klauzule G
Dokazujeme nesplnitelnost
(1) P  (X)(G1(X)  G2(X)      Gn(X))
kde G = {G1, G2,    , Gn} a X je vektor proměnných v G
nesplnitelnost (1) je ekvivalentní tvrzení (2) a (3)
(2) P G
(3) P (X)(G1(X)      Gn(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
Důkaz nesplnitelnosti P  {G} znamená nalezení protipříkladu
ten pomocí SLD-stromu konstruuje termy (odpověd') splňující konjunkci v (3)
Hana Rudová, Logické programování I, 30. března 2007 16 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, 30. března 2007 17 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ět'ová náročnost
složité řídící struktury
Hana Rudová, Logické programování I, 30. března 2007 17 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ět'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ět'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, 30. března 2007 17 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
(1) (3)
(2)
:- q.
:- r.
:- q.
Implementace SLD-rezoluce v Prologu
není úplná
logický program: q : -r. (1)
r : -q. (2)
q. (3)
dotaz: : -q.
Hana Rudová, Logické programování I, 30. března 2007 18 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)).
vede k: [B/X], [X/f(X)]
Unifikátor pro g(X1, . . . , Xn) a g(f(X0, X0), f(X1, X1), . . . , f(Xn-1, Xn-1))
X1 = f(X0, X0), X2 = f(X1, X1), . . . , Xn = f(Xn-1, Xn-1)
X2 = f(f(X0, X0), f(X0, X0)), . . .
délka termu pro Xk exponenciálně narůstá
Hana Rudová, Logické programování I, 30. března 2007 19 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)).
vede k: [B/X], [X/f(X)]
Unifikátor pro g(X1, . . . , Xn) a g(f(X0, X0), f(X1, X1), . . . , f(Xn-1, Xn-1))
X1 = f(X0, X0), X2 = f(X1, X1), . . . , Xn = f(Xn-1, Xn-1)
X2 = f(f(X0, X0), f(X0, X0)), . . .
délka termu pro Xk 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 = f(f(f(f(f(f(f (f(f(f(...))))))))))
Hana Rudová, Logické programování I, 30. března 2007 19 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(...)))))))))) problém se projeví
Hana Rudová, Logické programování I, 30. března 2007 20 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(...)))))))))) 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, 30. března 2007 20 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(...)))))))))) 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)
Řešení: problém typu (2) převést na problém typu (1) ?
Hana Rudová, Logické programování I, 30. března 2007 20 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(...)))))))))) 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)
Ř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, 30. března 2007 20 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(...)))))))))) 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)
Ř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.
optimalizace v kompilátoru mohou způsobit opět odpověd' ,,yes"
Hana Rudová, Logické programování I, 30. března 2007 20 Rezoluce a logické programování
Řízení implementace: řez
řez se syntakticky chová jako kterýkoliv jiný literál
:- p.
:- q,!,v.
ořezání
upnutí
nemá ale žádnou deklarativní sémantiku
místo toho mění implementaci programu
p : -q, !, v.
Hana Rudová, Logické programování I, 30. března 2007 21 Rezoluce a logické programování
Řízení implementace: řez
řez se syntakticky chová jako kterýkoliv jiný literál
:- p.
:- q,!,v.
ořezání
upnutí
nemá ale žádnou deklarativní sémantiku
místo toho mění implementaci programu
p : -q, !, v.
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
Hana Rudová, Logické programování I, 30. března 2007 21 Rezoluce a logické programování
Řízení implementace: řez
řez se syntakticky chová jako kterýkoliv jiný literál
:- p.
:- q,!,v.
ořezání
upnutí
nemá ale žádnou deklarativní sémantiku
místo toho mění implementaci programu
p : -q, !, v.
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í
Hana Rudová, Logické programování I, 30. března 2007 21 Rezoluce a logické programování
Příklad: řez
(1) (2)
(7)
(5)
(3)
fail
(!)
[X/a]
:- s.:- p,r.
:- !,v,r.
:- v,r.
:- t.
:- q(X),!,v,r.
t : -p, r. (1)
t : -s. (2)
p : -q(X), !, v. (3)
p : -u, w. (4)
q(a). (5)
q(b). (6)
s. (7)
u. (8)
Hana Rudová, Logické programování I, 30. března 2007 22 Rezoluce a logické programování
Příklad: řez II
(1)
(6) (7)
[X/2,Y/3] (3)
fail
(rez)
:- c(3).
:- !,c(3).
:- b(X,Y),!,c(Y).
:- a(X).
:- s(X).
a(X) : -b(X, Y), !, c(Y). (1)
a(X) : -c(X). (2)
b(2, 3). (3)
b(1, 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í I, 30. března 2007 23 Rezoluce a logické programování
Příklad: řez III
(1)
fail
(6)
(rez)
(5)
(7)
(4) [X/1,Y/2][X/2,Y/3] (3)
[X/1]
:- b(X,Y),c(Y),!.
:- c(3),!.
:- !.
:- a(X).
:- s(X).
:- c(2),!.
a(X) : -b(X, Y), c(Y), !. (1)
a(X) : -c(X). (2)
b(2, 3). (3)
b(1, 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í I, 30. března 2007 24 Rezoluce a logické programování