Lineární rezoluce Rezoluce a logické programování C o B o varianta rezoluční metody ■ snaha o generování lineární posloupnosti místo stromu ■ v každém kroku kromě prvního můžeme použít bezprostředně předcházející rezolventu a k tomu buď některou z klauzulí vstupní množiny S nebo některou z předcházejících rezolvent lineární rezoluční důkaz C z S je posloupnost dvojic , ■■■ (Cn,Bn) taková, že C = Cn+1 a ■ Q a každá Bi jsou prvky S nebo některé C,, j < í ■ každá Ci+i, í < n je rezolventa d a Bi '■ lineární vyvrácení S = lineární rezoluční důkaz □ z S C„ B„ \/ C \/ C, B j \/ C, B7 Hana Rudová, Logické programování I, 2. dubna 201 3 Rezoluce a logické programování Lineární rezoluce II. Prologovská notace příklad: S = {Ai, A2, A3, A4} Ai = {p,q} A2 = {p, -^q] Aj, = {^p,q} A4 = {^p, -^q] S: vstupní množina klauzulí (',: střední klauzule B{. boční klauzule C i B i {p,q}{p, -iq} \/ (pí l^p,q} \/ iq] {-Ti V ■ ■ ■ V ->Tn Jí -iTi V ■ ■ ■ V ~, ■ ■ ■ (Cn,Bn) taková, že C = Cn+i a ■ Co a každá Bí jsou prvky P 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+\ a ■ Co = G a každá K, JSOU prvky P lineární rezoluce + vstupní rezoluce ■ každá Cf+i, i < n je rezolventa Q a Bí Hana Rudová, Logické programování I, 2. dubna 2013 Rezoluce a logické programování Začneme s cílovou klauzulí: Co = G Boční klauzule vybíráme z programových klauzulí P G ={-q,-p} P= {Pi,P2,P3} : Pi = {p}, P2 = {p,^q}, P3 = iq) :-q,p. p. P--q, q. {^q,^p} Iq} \/, , {^q,^p} iq] í^pJ íp'^qí \/ \/ {-ip} (pJ {^ql M \/ \/ □ □ Střední klauzule jsou cílové klauzule Hana Rudová, Logické programování I, 2. dubna 201 3 Rezoluce a logické programování Cíle a fakta při lineární rezoluci 1 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 1 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, 2. dubna 2013 8 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 Ll-rezoluce pro Hornovy klauzule: Nechť P je množina programových klauzulí a G cílová klauzule. Je-li množina P u {G} Hornových klauzulí nesplnitelná, pak existuje rezoluční vyvrácení P u {G} pomocí Ll-rezoluce. ■ vstupní rezoluce pro (obecnou) formuli sama o sobě není úplná => 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 -iGm) ■ 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, 2. dubna 2013 9 Rezoluce a logické programování Uspořádané klauzule II. Uspořádané klauzule _{^A0,..., ~>An}_{B, -i_Bq, ..., -^Bm}_ {-*A0,-lAi-i, -ifioP, ■ ■ ■, -'Bmp, -lAi+i,-^An}a Hornovy klauzule _: -Ap,... ,An._B : -B0,... ,Bm._ : - (A0, ...,Ai-i,B0p,..., Bmp,Ai+i, ...,An)a. Příklad: {-*(*), -.t(l), -^u(X)} {ř(Z), -.q(Z, A"), -.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] a = [Z/l] Hana Rudová, Logické programování I, 2. dubna 201 3 11 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, -i_Bq, ..., -^Bm}_ {-*A0,-lAf-i, -ifioP, ■ ■ ■, ^Bmp, -lAf+i,..., ^An}a ■ uspořádaná rezolventa: {-*Ao....."vlí-i, ~^Bop.....-,-Bmp, -vií+i.....^An}a ■ p je přejmenování proměnných takové, že klauzule {Ao.....An\ a {B,Bo.....Bm}p nemají společné proměnné ■ potenciální instanciace proměnné ve vstupní cílové klauzuli Výsledná substituce (answer substitution) 9 = 9q9i ■ ■ ■ 9n složení unifikací Hana Rudová, Logické programování I, 2. dubna 2013 Rezoluce a logické programování Hana Rudová, Logické programování I, 2. dubna 2013 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 = {-iGi, -^Gz, ■ ■ ■ , ^Gn} a X je vektor proměnných v G nesplnitelnost (1) je ekvivalentní tvrzení (2) a (3) (2) P h -iG (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, 2. dubna 201 3 1 9 Rezoluce a logické programování