Rezoluce a logické programování Lineární rezoluce varianta rezoluční metody -fc snaha o generování lineární posloupnosti místo stromu -i- v každém kroku krome prvního mUžeme použít bezprostredne predcházející rezolventu a k tomu bud' nekterou z klauzulí vstupní množiny S nebo nekterou z predcházejících rezolvent C 0^/rB0 C2 B2 C Hana Rudová, Logické programování I, 2. dubna 2013 2 Rezoluce a logické programování Lineární rezoluce varianta rezoluční metody snaha o generování lineární posloupnosti místo stromu v každém kroku krome prvního mUžeme použít bezprostredne předcházející rezolventu a k tomu bud' nekterou z klauzulí vstupní množiny S nebo nekterou z predcházejících rezolvent lineární rezoluCní důkaz C z S je posloupnost dvojic Q: strední klauzule & B{. boCní klauzule C Bi {p,q}{p, -1 q} {p} {^p,q} IX □ Hana Rudová, Logické programování I, 2. dubna 2013 3 Rezoluce a logické programování Prologovská notace & Klauzule v matematické logice {Hi, ■■■ ,Hm,— Ti, ■■■ ,-Tn} Hi V--- V Hm V — Ti V ■ ■ ■ V -Tn Hana Rudová, Logické programování I, 2. dubna 2013 4 Rezoluce a logické programování Prologovská notace & Klauzule v matematické logice {Hi, ■■■ ,Hm,— Ti, ■■■ ,-Tn} Hi v--- v Hm v — Ti v ■ ■ ■ v — Tn & Hornova klauzule: nejvýše jeden pozitivní literál {H, —Ti,..., —Tn} {H} { — Ti,..., —Tn} a H V —Ti v ■ ■ ■ v —Tn H —Ti V ■ ■ ■V —Tn Hana Rudová, Logické programování I, 2. dubna 2013 4 Rezoluce a logické programování Prologovská notace & Klauzule v matematické logice {Hi, ■■■ ,Hm,— Ti, ■■■ ,— Tn} Hi V--- V Hm V — Ti V ■ ■ ■ V — Tn ii> Hornova klauzule: nejvýše jeden pozitivní literal {H, —Ti,..., —Tn} {H} { — Ti,..., —Tn} a H V —Ti V ■ ■ ■ V — Tn H —Ti V ■ ■ ■ V —Tn JS> Pravidlo: jeden pozitivní a alespoň jeden negativní literal Prolog: H : - Ti, ■ ■ ■ ,Tn. Hana Rudová, Logické programování I, 2. dubna 2013 4 Rezoluce a logické programování Prologovská notace & Klauzule v matematické logice {Hi, ■■■ ,Hm, —Ti, ■■■ , —Tn} Hi v ■■■v Hm v —Ti v ■ ■ ■ v —Tn & Hornova klauzule: nejvýše jeden pozitivní literál {H, —Ti,..., —Tn} {H} { — Ti,..., —Tn} a H v —Ti v ■ ■ ■v —Tn H —Ti v ■ ■ ■v —Tn JS> Pravidlo: jeden pozitivní a alespon jeden negativní literál J* Prolog: H : - Ti, ■ ■ ■ ,Tn. Matematická logika: H <= Ti a ■ ■ ■ a Tn Hana Rudová, Logické programování I, 2. dubna 2013 4 Rezoluce a logické programování Prologovská notace & Klauzule v matematické logice {Hi, --- ,Hm,-Ti, --- ,-Tn} Hi v ---v Hm v -Ti v - - - v -Tn & Hornova klauzule: nejvýše jeden pozitivní literal {H,-Ti,...,-Tn} {H} {-Ti,...,-Tn} a H v -Ti v - - - v -Tn H -Ti v - - - v -Tn JS> Pravidlo: jeden pozitivní a alespoň jeden negativní literal & Prolog: H : - Ti, - - - ,Tn. Matematická logika: H <= Ti a - - - a Tn H <= T Hana Rudová, Logické programování I, 2. dubna 2013 4 Rezoluce a logické programování Prologovská notace & Klauzule v matematické logice {Hi, ■■■ ,Hm,— Ti, ■■■ ,-Tn} Hi v--- v Hm v — Ti v ■ ■ ■ v — Tn & Hornova klauzule: nejvýše jeden pozitivní literál {H, —Ti,..., —Tn} {H} { — Ti,..., —Tn} a H v —Ti v ■ ■ ■ v —Tn H —Ti v ■ ■ ■v —Tn JS> Pravidlo: jeden pozitivní a alespon jeden negativní literál J* Prolog: H : - Ti, ■ ■ ■ ,Tn. Matematická logika: H <= Ti a ■ ■ ■ a Tn Hana Rudová, Logické programování I, 2. dubna 2013 4 Rezoluce a logické programování Prologovská notace & Klauzule v matematické logice {Hi, --- ,Hm,-Ti, --- ,-Tn} Hi v ---v Hm v -Ti v - - - v -Tn & Hornova klauzule: nejvýše jeden pozitivní literal {H,-Ti,...,-Tn} {H} {-Ti,...,-Tn} a H v -Ti v - - - v -Tn H -Ti v - - - v -Tn JS> Pravidlo: jeden pozitivní a alespoň jeden negativní literal & Prolog: H : - Ti, - - - ,Tn. Matematická logika: H <= Ti a - - - a Tn J* H <= T H v-T H v-Ti v---v-Tn Hana Rudová, Logické programování I, 2. dubna 2013 4 Rezoluce a logické programování Prologovská notace & Klauzule v matematické logice {Hi, --- ,Hm,— Ti, --- ,-Tn} Hi v ---v Hm v —Ti v - - - v — Tn & Hornova klauzule: nejvýše jeden pozitivní literál {H, —Ti,..., —Tn} {H} { — Ti,..., —Tn} a H v —Ti v - - - v —Tn H —Ti v - - - v —Tn JS> Pravidlo: jeden pozitivní a alespon jeden negativní literál J* Prolog: H : - Ti, - - - ,Tn. Matematická logika: H <= Ti a - - - a Tn M» H <= T H v—T H v—Ti v---v—Tn Klauzule: {H, —Ti,..., —Tn} Hana Rudová, Logické programování I, 2. dubna 2013 4 Rezoluce a logické programování Prologovská notace & Klauzule v matematické logice {Hi, ■■■ ,Hm, —Ti, ■■■ , —Tn} Hi v — v Hm v — Ti v ■ ■ ■ v — Tn & Hornova klauzule: nejvýše jeden pozitivní literál {H, —Ti,..., —Tn} {H} { — Ti,..., —Tn} a H v —Ti v ■ ■ ■ v — Tn H —Ti v ■ ■ ■ v — Tn JS> Pravidlo: jeden pozitivní a alespon jeden negativní literál J* Prolog: H : - Ti, ■ ■ ■ ,Tn. Matematická logika: H <= Ti a ■ ■ ■ a Tn M» H <= T H v—T H v — Ti v ■ ■ ■ v — Tn Klauzule: {H, —Ti,..., —Tn} -í* Fakt: pouze jeden pozitivní literál Prolog: H. Matematická logika: H Klauzule: {H} Hana Rudová, Logické programování I, 2. dubna 2013 4 Rezoluce a logické programování Prologovská notace -i* Klauzule v matematické logice (Hi, ■■■ ,Hm,-Ti, ■■■ ,-Tn} Hi v ■■■v Hm v -Ti v ■ ■ ■ v -Tn ü> Hornova klauzule: nejvýše jeden pozitivní literál (H,-Ti,...,-Tn} (H} (-Ti,...,-Tn} a H v -T1 v ■ ■ ■v -Tn H -T1 v ■ ■ ■v -Tn JS> Pravidlo: jeden pozitivní a alespon jeden negativní literál & Prolog: H : - T1, ■ ■ ■ ,Tn. Matematická logika: H <= T1 a ■ ■ ■ a Tn M» H <= T H v-T H v-T1 v ■ ■ ■ v -Tn Klauzule: (H,-T1,..., -Tn} Fakt: pouze jeden pozitivní literál Prolog: H. Matematická logika: H Klauzule: (H} & Cílová klauzule: žádný pozitivní literál it Prolog: : - T1,... Tn. Matematická logika: -T1 v ■ ■ ■ v -Tn Klauzule: (-T1, ■ ■ ■ -Tn} Hana Rudová, Logické programování I, 2. dubna 2013 4 Rezoluce a logické programování Logický program Programová klauzule: práve jeden pozitivní literál (fakt nebo pravidlo) Logický program: konecná množina programových klauzulí Príklad: Sľ logický program jako množina klauzulí: P = {P1.P2.P3} Pi ={p}, P2 = {p, -q}, P3 = {q} Hana Rudová, Logické programování I, 2. dubna 2013 5 Rezoluce a logické programování Logický program Programová klauzule: práve jeden pozitivní literál (fakt nebo pravidlo) Logický program: konecná množina programových klauzulí Príklad: a logický program jako množina klauzulí: P = {Pi,P2,P3} Pi = {p}, P2 = {p, —q}, P3 = {q} & logický program v prologovské notaci: p. p: -q. q. a cílová klauzule: G = {—q, —p} : -q, p. Hana Rudová, Logické programování I, 2. dubna 2013 5 Rezoluce a logické programování Lineární rezoluce pro Hornovy klauzule & ZaCneme s cílovou klauzulí: C0 = G ií> Bocní klauzule vybíráme z programových klauzulí P M G = {-q,-p} P ={Pi,P2,P3} : Pi = {p}, P2 = {p, -q}, P3 = {q} : -q, p. p. p : -q, q. Hana Rudová, Logické programování I, 2. dubna 2013 6 Rezoluce a logické programování Lineární rezoluce pro Hornovy klauzule St Zacneme s cílovou klauzulí: C0 = G St Bocní klauzule vybíráme z programových klauzulí P MG = {-q,-p} P ={Pi,P2,P3} : Pi = {p}, P2 = {p, -q}, P3 = {q} * : -q,p- p. p: -q, q. (fl (Pi Hana Rudová, Logické programování I, 2. dubna 2013 6 Rezoluce a logické programování Lineární rezoluce pro Hornovy klauzule JS* Zacneme s cílovou klauzulí: Co = G St Bocní klauzule vybíráme z programových klauzulí P MG = {-q,-p} P ={Pi,Pz,P3} : Pi = {p}, P2 = {p, -q}, P3 = {q} * : -q,p. p. p: -q, q. {~ Strední klauzule jsou cílové klauzule Hana Rudová, Logické programování I, 2. dubna 2013 6 Rezoluce a logické programování Lineární vstupní rezoluce Vstupní rezoluce na P u {G} S» (opakování:) alespoň jedna z klauzulí použitá při rezoluci je z výchozí vstupní množiny & zacneme s cílovou klauzulí: Co = G & bocní klauzule jsou vždy z P (tj. jsou to programové klauzule) Hana Rudová, Logické programování I, 2. dubna 2013 7 Rezoluce a logické programování Lineární vstupní rezoluce Vstupní rezoluce na P u {G} -i* (opakování:) alespoň jedna z klauzulí použitá pri rezoluci je z výchozí vstupní množiny & zacneme s cílovou klauzulí: Co = G & bocní klauzule jsou vždy z P (tj. jsou to programové klauzule) (Opakování:) Lineární rezoluCní dukaz C z P je posloupnost dvojic (Co,Bo>, ... (Cn,Bn) taková, že C = Cn+i a k C0 a každá Bi jsou prvky P nebo nekteré Cj,j < i S» každá Ci+i, i < n je rezolventa Ci a Bi Hana Rudová, Logické programování I, 2. dubna 2013 7 Rezoluce a logické programování Lineární vstupní rezoluce & Vstupní rezoluce na P u {G} S» (opakování:) alespoň jedna z klauzulí použitá pri rezoluci je z výchozí vstupní množiny & zacneme s cílovou klauzulí: C0 = G & bocní klauzule jsou vždy z P (tj. jsou to programové klauzule) JS* (Opakování:) Lineární rezolucní dukaz C z P je posloupnost dvojic (Co,Bo), ... (Cn,Bn) taková, že C = Cn+i a C0 a každá Bi jsou prvky P nebo nekteré Cj,j < i S» každá Ci+1, i < n je rezolventa Ci a Bi Lineární vstupní (Linear Input) rezoluce (LI-rezoluce) C z P u {G} posloupnost dvojic {C0,B0), ... {Cn,Bn) taková, že C = Cn+1 a a C0 = G a každá Bi jsou prvky P lineární rezoluce + vstupní rezoluce a každá Ci+1, i < n je rezolventa Ci a Bi Hana Rudová, Logické programování I, 2. dubna 2013 7 Rezoluce a logické programování Cíle a fakta pri lineární rezoluci JS> Veta: Je-li S nesplnitelná množina Hornových klauzulí, pak S obsahuje alespon 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 alespon jeden negat. literál), pri rezoluci mi stále zustává alespon jeden pozit. literál Hana Rudová, Logické programování I, 2. dubna 2013 8 Rezoluce a logické programování Cíle a fakta při lineární rezoluci & Veta: 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 alespon jeden negat. literál), pri rezoluci mi stále zustává alespon jeden pozit. literál & pokud nepoužiji fakt, mám pouze cíle (negat.literály) a pravidla (1 pozit.literál a alespon jeden negat. literál), v rezolvente mi stále zustávají negativní literály Hana Rudová, Logické programování I, 2. dubna 2013 8 Rezoluce a logické programování Cíle a fakta pri lineární rezoluci JS> Veta: Je-li S nesplnitelná množina Hornových klauzulí, pak S obsahuje alespon 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 alespon jeden negat. literál), pri rezoluci mi stále zustává alespon jeden pozit. literál -fc pokud nepoužiji fakt, mám pouze cíle (negat.literály) a pravidla (1 pozit.literál a alespon jeden negat. literál), v rezolvente mi stále zustávají negativní literály veta: Existuje-li rezolucní důkaz prázdné množiny z množiny S Hornových klauzulí, pak tento rezolucní strom má v listech jedinou cílovou klauzuli. pokud zacnu dukaz pravidlem a faktem, pak dostanu zase pravidlo -i- pokud zacnu dukaz dvema pravidly, pak dostanu zase pravidlo A na dvou faktech rezolvovat nelze Hana Rudová, Logické programování I, 2. dubna 2013 8 Rezoluce a logické programování Cíle a fakta pri lineární rezoluci JS> Veta: 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 alespon jeden negat. literál), pri rezoluci mi stále zůstává alespon jeden pozit. literál & pokud nepoužiji fakt, mám pouze cíle (negat.literály) a pravidla (1 pozit.literál a alespon jeden negat. literál), v rezolvente mi stále zustávají negativní literály veta: Existuje-li rezolucní dukaz prázdné množiny z množiny S Hornových klauzulí, pak tento rezolucní strom má v listech jedinou cílovou klauzuli. pokud zacnu dukaz pravidlem a faktem, pak dostanu zase pravidlo -i- pokud zacnu dukaz dvema pravidly, pak dostanu zase pravidlo -fc na dvou faktech rezolvovat nelze = dokud nepoužiji cíl pracuji stále s množinou faktu a pravidel Hana Rudová, Logické programování I, 2. dubna 2013 8 Rezoluce a logické programování Cíle a fakta pri lineární rezoluci JS> Veta: Je-li S nesplnitelná množina Hornových klauzulí, pak S obsahuje alespon 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 alespon jeden negat. literál), při rezoluci mi stále zůstává alespon jeden pozit. literál -fc pokud nepoužiji fakt, mám pouze cíle (negat.literály) a pravidla (1 pozit.literál a alespon jeden negat. literál), v rezolvente mi stále zustávají negativní literály veta: Existuje-li rezolucní dukaz prázdné množiny z množiny S Hornových klauzulí, pak tento rezolucní strom má v listech jedinou cílovou klauzuli. pokud zacnu dukaz pravidlem a faktem, pak dostanu zase pravidlo -i- pokud zacnu dukaz dvema pravidly, pak dostanu zase pravidlo A na dvou faktech rezolvovat nelze => dokud nepoužiji cíl pracuji stále s množinou faktu a pravidel ± pokud použiji v dukazu cílovou klauzulí, fakta mi ubírají negat.literály, pravidla mi je pridávají, v rezolvente 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 Veta: Množina S Hornových klauzulí je nesplnitelná, práve když existuje rezolucní vyvrácení S pomocí vstupní rezoluce. M Korektnost platí stejne 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 u {G} Hornových klauzulí nesplnitelná, pak existuje rezolucní vyvrácení P u {G} pomocí LI-rezoluce. A vstupní rezoluce pro (obecnou) formuli sama o sobe není úplná => LI-rezoluce aplikovaná na (obecnou) formuli nezarucuje, že nalezeneme dukaz, i když formule platí! Hana Rudová, Logické programování I, 2. dubna 2013 9 Rezoluce a logické programování Korektnost a úplnost Veta: Množina S Hornových klauzulí je nesplnitelná, práve když existuje rezolucní vyvrácení S pomocí vstupní rezoluce. M Korektnost platí stejne 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 u {G} Hornových klauzulí nesplnitelná, pak existuje rezolucní vyvrácení P u {G} pomocí LI-rezoluce. A vstupní rezoluce pro (obecnou) formuli sama o sobe není úplná => LI-rezoluce aplikovaná na (obecnou) formuli nezarucuje, že nalezeneme dukaz, i když formule platí! & Význam LI-rezoluce pro Hornovy klauzule: i* P = {Pi, . . . , Pn}, G = {G i ,...,Gm} iľ LI-rezolucí ukážeme nesplnitelnost Pi a - - - a Pn a (—Gi v - - - v —Gm) Hana Rudová, Logické programování I, 2. dubna 2013 9 Rezoluce a logické programování Korektnost a úplnost Veta: Množina S Hornových klauzulí je nesplnitelná, práve když existuje rezolucní vyvrácení S pomocí vstupní rezoluce. M Korektnost platí stejne 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 u {G} Hornových klauzulí nesplnitelná, pak existuje rezolucní vyvrácení P u {G} pomocí LI-rezoluce. A vstupní rezoluce pro (obecnou) formuli sama o sobe není úplná => LI-rezoluce aplikovaná na (obecnou) formuli nezarucuje, že nalezeneme dukaz, i když formule platí! & Význam LI-rezoluce pro Hornovy klauzule: i* P = {Pi, . . . , Pn}, G = {G i ,...,Gm} iľ LI-rezolucí ukážeme nesplnitelnost Pi a ■ ■ ■ a Pn a (—Gi v ■ ■ ■ v —Gm) pokud tedy predpokládáme, že program {Pi,.. .,Pn} platí, tak musí být nepravdivá (—Gi v ■ ■ ■ v —Gm), tj. musí platit Gi a ■ ■ ■ a Gm Hana Rudová, Logické programování I, 2. dubna 2013 9 Rezoluce a logické programování Usporádané klauzule (definite clauses) JS> Klauzule = množina literálu JS> Uspořádaná klauzule (definite clause) = posloupnost literálu it nelze volne menit poradí literálu £ RezoluCní princip pro usporádané klauzule: _{-Ao,-An}_[B1 -Bo,-Bm\_ M usporádaná rezolventa: {-A0,-Ai-\, -B0p,-Bmp,—Ai+\,-An}j &> p je prejmenování promenných takové, že klauzule {A0,.. .,An} a {B,B0,.. .,Bm}p nemají spolecné promenné & j je nejobecnejší unifikátor pro Ai a Bp Hana Rudová, Logické programování I, 2. dubna 2013 10 Rezoluce a logické programování Usporádané klauzule (definite clauses) JS> Klauzule = množina literálu JS> Uspořádaná klauzule (definite clause) = posloupnost literálu it nelze volne menit poradí literálu £ RezoluCní princip pro usporádané klauzule: _{-Ao,-An}_[B1 -Bo,-Bm\_ {-Ao,-Ai-i, -Bop,-BmP,-At+i,-An} j M usporádaná rezolventa: {-A0,-Ai-\, -B0p,-Bmp,—Ai+\,-An}j &> p je prejmenování promenných takové, že klauzule {A0,.. .,An} a {B,B0,.. .,Bm}p nemají spolecné promenné & j je nejobecnejší unifikátor pro Ai a Bp it rezoluce je realizována na literálech -Aij a Bpj Jt je dodržováno poradí literálu, tj. {-B0p,-Bmp}j jde do usporádané rezolventy presne na pozici -Aij Hana Rudová, Logické programování I, 2. dubna 2013 10 Rezoluce a logické programování Usporádané klauzule II. C Usporádáné klauzule _{— Ao,—An}_{B, —Bo,—Bm\_ {—Ao,—Ai-i, —Bop,—BmP,—Ai+i,—An} LD-rezoluce: korektní a úplná Hana Rudová, Logické programování I, 2. dubna 2013 12 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, 2. dubna 2013 13 Rezoluce a logické programování SLD-rezoluce JS> 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 (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álu R(C) e C -i- pri rezoluci vybírám z klauzule literál urcený selekcním pravidlem Hana Rudová, Logické programování I, 2. dubna 2013 13 Rezoluce a logické programování SLD-rezoluce JS> 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álů R(C) e 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 literálu nejlevejší literál vybírá i Prolog Hana Rudová, Logické programování I, 2. dubna 2013 13 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 | výber | y/ nejlevejšího {^P} Jp} nejpravejšího Jq} literálu I / literálu ' ^ □ □ Hana Rudová, Logické programování I, 2. dubna 2013 14 Rezoluce a logické programování Lineární rezoluce se selekcním pravidlem P = {{p}, {p, -q}, {q}}, G = {-q,-p} {^q,^p} {q} {^q,^p} {p} výber | výber | y/ nejlevejšího {^P} Jpl nejpravejšího Jq} literálu ' / literálu ' ^ □ □ SLD-rezolucní vyvrácení P u {G} pomocí selekcního pravidla R je LD-rezolucní vyvrácení (G0,C0),(Gn,Cn) takové, že G = G0,Gn+i = D a R(Gi) je literál rezolvovaný v kroku i Hana Rudová, Logické programování I, 2. dubna 2013 14 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í ,{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 & způsobu 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, 2. dubna 2013 14 Rezoluce a logické programování Příklad: SLD-strom t: -p,r. t : -s. p : -q, v. p : - u, w q. s. u. (D (2) (3) (4) (5) (6) (7) : -1. (D/\ (2) :-p,r. (3)/ \(4) :- s. (5) :- v,r. fall :- u,w,r. (7) :- w,r. .(6) □ fall Hana Rudová, Logické programování I, 2. dubna 2013 15 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, 2. dubna 2013 16 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 korenem stromu je cílová klauzule G v uzlech stromu jsou rezolventy (rodiče uzlu a programové klauzule) Jt císlo vybrané programové klauzule pro rezoluci je v príkladu uvedeno jako ohodnocení hrany listy jsou dvojího druhu: a 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, 2. dubna 2013 16 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 korenem stromu je cílová klauzule G v uzlech stromu jsou rezolventy (rodice uzlu a programové klauzule) & císlo vybrané programové klauzule pro rezoluci je v príkladu uvedeno jako ohodnocení hrany listy jsou dvojího druhu: a 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) ú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, 2. dubna 2013 16 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, 2. dubna 2013 17 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). Cvicení: 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/i] a [Z/2] nezajímá me substituce [Y/2] Hana Rudová, Logické programování I, 2. dubna 2013 17 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, 2. dubna 2013 18 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] JS> 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, 2. dubna 2013 18 Rezoluce a logické programování Význam SLD-rezolucního vyvrácení P u {G} C 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, 2. dubna 2013 19 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, 2. dubna 2013 19 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 = {-Gi, -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 objektů, které na základe vlastností množiny P splnují konjunkci literálu v cílové klauzuli Hana Rudová, Logické programování I, 2. dubna 2013 19 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 = { — 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 -i* 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, 2. dubna 2013 19 Rezoluce a logické programování