Logický program Rezoluce a logické programování (pokračování) ■ 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} Pi = {p], Pz = {p,^q}, P3={q] ■ logický program v prologovské notaci: P- p ■ -a- q. ■ cílová klauzule: G = {^q, -^p} : -q, p. Lineární rezoluce pro Hornovy klauzule Začneme s cílovou klauzulí: Co = G Boční klauzule vybíráme z programových klauzulí P G={-.q,-.p} P = {P1.P2.P3} '■ Pi = {p}, P2 = {p,^q}, P3 = W p. p : -q, q. -q.p. {-pj (qJ \/ \/ {-p} (pi {^ql (íl \/ \/ □ □ Střední klauzule jsou cílové klauzule Hana Rudová, Logické programování I, 30. března 2007 Rezoluce a logické programování Hana Rudová, Logické programování I, 30. března 2007 Rezoluce a logické programování Lineární vstupní rezoluce Vstupní rezoluce na P u {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í: Co = 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 (Cq.Bq), ... {Cn.Bn) taková, že C = Cn+i a ■ Co a každá Bí jsou prvky S nebo některé Cj.j < í ■ každá Cí+i, í < n je rezolventa C; a Bí Lineární vstupní (Linear ínput) rezoluce (Ll-rezoluce) C z P u {G} posloupnost dvojic (Co,Bo), ■ ■ ■ (Cn,Bn) taková, že C = Cn+i a ■ Co = G a každá Bí jsou prvky P ■ každá Cf+i, i < n je rezolventa Q a Bí lineární rezoluce + vstupní rezoluce Hana Rudová, Logické programování I, 30. března 2007 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 požit.literál) a pravidla (1 požit.literál a alespoň jeden negat. literál), při rezoluci mi stále zůstává alespoň jeden požit, literál ■ pokud nepoužiji fakt, mám pouze cíle (negat.literály) a pravidla (1 požit.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í Uspořádané klauzule (definite clauses) ■ Klauzule = množina literálů ■ Uspořádaná klauzule (depnite clause) = posloupnost literálů ■ nelze volně měnit pořadí literálů ■ Rezoluční princip pro uspořádané klauzule: _{^Ao,..., ->An}_{B, -i_Bq, ..., -^Bm}_ {-*A0,-iAí-i, -ifioP, ■ ■ ■, ^Bmp, -lAf+i,..., ^An}a ■ uspořádaná rezolventa: {-*Ao.....~vlí-i, -*Bop.....^Bmp, -■Aí+i.....-iAn}cr ■ p je přejmenování proměnných takové, že klauzule {Aq.....An\ a {B,Bq.....Bm}p nemají společné proměnné ■ Ll-rezoluce aplikovaná na (obecnou) formuli nezaručuje, že nalezeneme důkaz, i když formule platí! ■ Význam Ll-rezoluce pro Hornovy klauzule: ■ P = ÍPi.....Pn), G = {Gi.....Gm] ■ Ll-rezolucí ukážeme nesplnitelnost P\ a ■ ■ ■ a Pn a (-iGi v ■ ■ ■ v ^Gm) ■ pokud tedy předpokládáme, že program {P\.....Pn\ platí, tak musí být nepravdivá (-iGi v ■ ■ ■ v -iGm), tj. musí platit Gi a ■ ■ ■ a Gm Hana Rudová, Logické programování I, 30. března 2007 6 Rezoluce a logické programování Uspořádané klauzule II. ■ Uspořádané klauzule _{^A0,..., -^An}_{B, ->Bp,..., -^Bm}_ {-*A0,-lAi-i, -ifioP, ■ ■ ■, -'Bmp, -*Ai+i,..., -^An}a Hornovy klauzule _: -Ap,... ,An._B : -B0,... ,Bm._ : - (A0,...,Ai-i,B0p,...,Bmp,Ai+i,...,An)a. ■ Příklad: {^s(X), -.t(l), -^u(X)} {t(Z),^q(Z,X), ^r(3)} {-.í(A-),-.q(l,A),-.r(3),-.u(A-)} : -s(X), t(l),u(X). ř(Z) : -q(Z,X),r(3). : -s(X),q(l,A),r(3),u(X). p = [X/A] a=[Z/l] Hana Rudová, Logické programování I, 30. března 2007 8 Rezoluce a logické programování LD-rezoluce SLD-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 = □ ■ Gi je uspořádaná cílová klauzule ■ Ci je přejmenování klauzule z P ■ Q neobsahuje proměnné, které jsou v Gj, j < í nebo v Q, fe < i ■ Gí+i,0 < i < n je uspořádaná rezolventa Gi a C/. LD-rezoluce: korektní a úplná Hana Rudová, Logické programování I, 30. března 2007 9 Rezoluce a logické programování ■ 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) e 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] {^q,^p} ÍPl {p, -iq}, {q}}, G = {^q, -ip} {^q,^p} Iq} výběr j y/ nejlevějšího M \ / literálu I / výběr nejpravějšího í-"?? M literálu I / □ □ 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+\ = □ 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, 30. března 2007 Rezoluce a logické programování Příklad: SLD-strom ř : -p,r. t: -s. P '■ -q,v. p : -u, w. q. s. u. (D (2) (3) (4) (5) (6) (7) (1 (2) (3)/ - p, r. q, v, r. (5) u,w,r. (7) w.r. v(6) □ fail fail Hana Rudová, Logické programování I, 30. března 2007 Rezoluce a logické programování Strom výpočtu (SLD-strom) Příklad: SLD-strom a výsledná substituce 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 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 (1) (2) (3) (4) (5) Hana Rudová, Logické programování I, 30. března 2007 Rezoluce a logické programování : -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í I, 30. března 2007 :- 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 = 9q9i ■ ■ ■ 0n složení unifikací Význam SLD-rezolučního vyvrácení P u {G} Množina P proaramový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í I, 30. března 2007 Rezoluce a logické programování Hana Rudová, Logické programování I, 30. března 2007 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í I, 30. března 2007 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átorpro0(*i,...,*n) ag(f(X0,X0),f(X1,X1),...,f(Xn-1,Xn-1)) Xi=f(Xo,Xo), X2 = 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í I, 30. března 2007 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í I, 30. března 2007 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, 30. března 2007 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^ňfeKrňlV^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í I, 30. března 2007 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í I, 30. března 2007 [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, 30. března 2007 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) ■ c(3),!. fail (4) [X/1 ,Y/2] ■ c(2)J. (5) . /_ (rez) □ [X/11 Hana Rudová, Logické programování I, 30. března 2007 Rezoluce a logické programování