Klaus´ aln´ı tvar mnoˇ ziny formul´ı Tvorba rezolvent — maxim´ aln´ı unifik´ ator Rezoluˇ cn´ı algoritmus
Rezoluce v predik´ atov´ e logice
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce v PL
1/16
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Tvorba rezolvent — maxim´ aln´ı unifik´ ator Rezoluˇ cn´ı algoritmus
Z´ akladn´ı myˇslenky 1
M |= ϕ iff X = M ∪ {¬ϕ} nesplniteln´a. (M mus´ı b´yt mnoˇzina sentenc´ı, ϕ sentence.)
2
X nesplniteln´a iff X |= ff.
3
Hled´an´ı kritick´ych“ d˚ usledk˚ u X syntakticky. K tomu je ” zapotˇreb´ı speci´aln´ı tvar X .
4
Speci´aln´ı tvar X je klaus´aln´ı tvar X .
Vˇse budeme dˇelat pro koneˇcnou mnoˇzinu M. Pak i X je koneˇcn´a. Tud´ıˇz: (syntaktick´y) algoritmus. V z´asadˇe stejn´y algoritmus jako ve VL, nˇekter´e kroky jsou vˇsak sloˇzitˇejˇs´ı — d´ano sloˇzitost´ı syntaxe PL.
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce v PL
2/16
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Tvorba rezolvent — maxim´ aln´ı unifik´ ator Rezoluˇ cn´ı algoritmus
Sentence v CNF ˇ Rekneme, ˇze ψ je v CNF, kdyˇz m´a tvar bud’ tt nebo ψ1 ∧ . . . ∧ ψn , kde 1 kaˇ zd´e ψi je sentence tvaru bud’ τi nebo ∀x1 .∀x2 . . . ∀xmi .τi 2
3
kaˇzd´e τi (tzv. tˇelo klausule ψi ) je bud’ ff nebo nebo `1 ∨ . . . ∨ `ki kaˇzd´e `j (liter´al) je bud’ atom nebo negace atomu.
Upozornˇ en´ı Nedefinujeme CNF jako synonymum. Pˇri hled´an´ı CNF m˚ uˇze doj´ıt ke zmˇenˇe jazyka: tzv. Skolemovo rozˇs´ıˇren´ı, neboli skolemisace.
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce v PL
3/16
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Tvorba rezolvent — maxim´ aln´ı unifik´ ator Rezoluˇ cn´ı algoritmus
Pˇrevod sentence ϕ na CNF 1
Vyˇciˇstˇen´ı v´yskytu promˇenn´ych: kaˇzd´y kvantifik´ator mus´ı v´azat jinou promˇennou. (α-konverse, to m˚ uˇze vyˇzadovat deklaraci fresh promˇenn´ych.)
2
Odstranˇen´ı nepohodln´ych spojek.
3
Distribuce ¬ tˇesnˇe pˇred atomy (de Morganova pravidla).
4
Distribuce ∨ na nejniˇzˇs´ı moˇznou hladinu (distributivn´ı a asociativn´ı z´akony — dalˇs´ı strana).
5
Distribuce ∧ na nejvyˇsˇs´ı moˇznou hladinu a eliminace existenˇcn´ıch kvantifik´ator˚ u (distributivn´ı a asociativn´ı z´akony a skolemisace — viz dalˇs´ı strany).
6
V´yslednou sentenci oznaˇc´ıme cnf(ϕ).
Obecnˇ e nedos´ ahneme ϕ |=| cnf(ϕ) Bude platit: ϕ a cnf(ϕ) jsou ekvisplniteln´e. Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce v PL
4/16
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Tvorba rezolvent — maxim´ aln´ı unifik´ ator Rezoluˇ cn´ı algoritmus
Nov´ e distributivn´ı a asociativn´ı z´ akony Plat´ı: 1
Asociativita ∀ a ∧: ∀x.(α ∧ β) |=| ∀x.α ∧ ∀x.β pro libovoln´e formule α, β.
2
Asociativita ∃ a ∨: ∃x.(α ∨ β) |=| ∃x.α ∨ ∃x.β pro libovoln´e formule α, β.
3
Distributivita ∀ a ∨: ∀x.(α ∨ β) |=| ∀x.α ∨ β pro libovoln´e formule α, β, kde v β se nevyskytuje x.
4
Distributivita ∃ a ∧: ∃x.(α ∧ β) |=| ∃x.α ∧ β pro libovoln´e formule α, β, kde v β se nevyskytuje x.
Intuice: ∀ je nekoneˇcn´e and a ∃ je nekoneˇcn´e or.
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce v PL
5/16
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Tvorba rezolvent — maxim´ aln´ı unifik´ ator Rezoluˇ cn´ı algoritmus
Skolemovo rozˇs´ıˇren´ı Sentenci ∀x1 . . . ∀xm .∃y .α,
m≥0
nahrad’te sentenc´ı ∀x1 . . . ∀xm .α[y := f (x1 , . . . , xm )] kde f je fresh funkˇcn´ı symbol arity m.
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce v PL
6/16
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Tvorba rezolvent — maxim´ aln´ı unifik´ ator Rezoluˇ cn´ı algoritmus
Pˇr´ıklad Najdˇete cnf(ϕ) pro sentenci ϕ ve tvaru ¬ ∀x.(P(x) ⇒ ∃y .Q(x, y )) ⇒ ¬∀x.(P(x) ⇒ ∃y .P(f (y ))) Pozorov´ an´ı Zjevnˇe pro obecnou sentenci ϕ plat´ı: ϕ a cnf(ϕ) jsou ekvisplniteln´e.
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce v PL
7/16
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Tvorba rezolvent — maxim´ aln´ı unifik´ ator Rezoluˇ cn´ı algoritmus
Klaus´ aln´ı tvar mnoˇ ziny sentenc´ı α ∈ kt(X ) iff α je klausule nˇejak´e cnf(ϕ) pro ϕ ∈ X . Upozornˇ en´ı kt(X ) nen´ı jednoznaˇcnˇe urˇcen! Pozorov´ an´ı X a kt(X ) jsou ekvisplniteln´e.
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce v PL
8/16
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Tvorba rezolvent — maxim´ aln´ı unifik´ ator Rezoluˇ cn´ı algoritmus
Komplement´ arn´ı v´ yskyt Dvˇe klausule ψ1 , ψ2 pro CNF obsahuj´ı komplement´arn´ı v´yskyt predik´atu P, pokud se v ψ1 vyskytuje P a v ψ2 se vyskytuje ¬P (nebo naopak). Pˇr´ıklady At’ f ∈ Pred arity 1, R ∈ Pred, arity 2 a x, y , u, v ∈ Var. 1
Klausule ∀x∀y (¬x = y ∨ ¬R(x, y )), ∀u∀v (¬u = v ∨ R(u, v )). Komplement´arn´ı v´yskyt predik´atu R.
2
Klausule ∀x∀y (¬x = y ∨ ¬R(x, f (y ))), ∀u∀v (¬u = v ∨ R(u, v )). Komplement´arn´ı v´yskyt predik´atu R.
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce v PL
9/16
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Tvorba rezolvent — maxim´ aln´ı unifik´ ator Rezoluˇ cn´ı algoritmus
Pˇr´ıklad, pokraˇ c. 3
Klausule ∀x∀y (x = y ∨ ¬R(x, f (y ))), ∀u∀v (¬u = f (v ) ∨ R(u, v )). Komplement´arn´ı v´yskyt predik´atu = a komplement´arn´ı v´yskyt predik´atu R.
4
Klausule ∀x∀y (x = y ∨ ¬R(x, f (y ))), ∀u∀v (u = f (v ) ∨ ¬R(u, v )). ˇ adn´y komplement´arn´ı v´yskyt predik´atu. Z´
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce v PL
10/16
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Tvorba rezolvent — maxim´ aln´ı unifik´ ator Rezoluˇ cn´ı algoritmus
Jak utvoˇrit resolventu dvou klausul´ı ψ1 a ψ2 1
Obsahuj´ı ψ1 a ψ2 komplement´arn´ı v´yskyt predik´atu? (Pokud ne, stop: resolventa neexistuje.)
2
Oznaˇcte predik´at s komplement´arn´ım v´yskytem jako P.
3
Existuje maxim´aln´ı unifik´ator pro atomy vytvoˇren´e z P? (Pokud ne, stop: resolventa podle P neexistuje.)
4
Oznaˇcte maxim´aln´ı unifik´ator jako ϑ.
5
Spoˇc´ıtejte ψ1 [ϑ] a ψ2 [ϑ]. Tˇela tˇechto klausul´ı oznaˇcte jako τ1 a τ2 .
6
Vytvoˇrte tˇelo, kter´e obsahuje vˇsechny liter´aly obsaˇzen´e v τ1 a τ2 kromˇe liter´al˚ u zaˇc´ınaj´ıc´ıch P a ¬P. Toto tˇelo oznaˇcte τ .
7
Tˇelo τ doplˇ nte obecn´ymi kvantifik´atory na sentenci.
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce v PL
11/16
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Tvorba rezolvent — maxim´ aln´ı unifik´ ator Rezoluˇ cn´ı algoritmus
Pˇr´ıklady: naleznˇ ete maxim´ aln´ı unifik´ ator 1
P(x, y ) a P(t, f (z)) (x, y , z, t st. promˇenn´e, P predik´at arity 2, f funkˇcn´ı symbol arity 1)
2
Q(a, y , f (y )) a Q(z, z, u) (x, y , z st. promˇenn´e, Q predik´at arity 3, f funkˇcn´ı symbol arity 1, a, u funkˇcn´ı symboly arity 0)
3
R(x, g (x)) a R(y , y ) (x, y st. promˇenn´e, R predik´at arity 2, g funkˇcn´ı symbol arity 1)
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce v PL
12/16
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Tvorba rezolvent — maxim´ aln´ı unifik´ ator Rezoluˇ cn´ı algoritmus
Definice At’ X 0 je koneˇcn´a mnoˇzina klausul´ı pro CNF. Posloupnost Res0 (X 0 ), Res1 (X 0 ), Res2 (X 0 ), Res3 (X 0 ), . . . definujeme takto: Res0 (X 0 ) = X 0 Resn+1 (X 0 ) = Resn (X 0 ) ∪ {α | α je resolventa nˇejak´e dvojice z Resn (X 0 )} Pozorov´ an´ı Ekvisplnitelnost je invariantem a tvorba posloupnosti mnoˇzin se zastav´ı po koneˇcnˇe kroc´ıch.
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce v PL
13/16
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Tvorba rezolvent — maxim´ aln´ı unifik´ ator Rezoluˇ cn´ı algoritmus
D˚ usledek: z´ akladn´ı resoluˇ cn´ı algoritmus 1
Rozhodnˇete, zda M |= ϕ (M koneˇcn´a).
2
Utvoˇrte X = M ∪ {¬ϕ}. At’ X 0 = kt(X ). Potom X 0 a X jsou ekvisplniteln´e. Existuje n0 tak, ˇze plat´ı Resn0 +1 (X 0 ) = Resn0 (X 0 ). D´ale plat´ı:
3 4
1 2
5
Mnoˇziny X 0 a Resn0 (X 0 ) jsou ekvisplniteln´e. Mnoˇzina X 0 nen´ı splniteln´a pr´avˇe tehdy, kdyˇz plat´ı ff ∈ Resn0 (X 0 ).
M |= ϕ plat´ı iff X 0 nen´ı splniteln´a.
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce v PL
14/16
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Tvorba rezolvent — maxim´ aln´ı unifik´ ator Rezoluˇ cn´ı algoritmus
Pozor! Na pˇredn´aˇsce bude zm´ınˇena i m´ırn´a varianta klasick´eho resoluˇcn´ıho algoritmu, kterou v tomto textu nenajdete. Tuto variantu (zam´ıtac´ı stromy, anglicky refutation trees) naleznete ve skriptu M. Demlov´a a B. Pondˇel´ıˇcek, Matematick´a logika, FEL ˇ CVUT, Praha 1997 Form´ aln´ı n´ astroje Vyzkouˇsejte si napˇr´ıklad volnˇe staˇziteln´y theorem prover Prover9 a Mace4 od Williama McCunea http://www.cs.unm.edu/∼mccune/prover9/
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce v PL
15/16
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Tvorba rezolvent — maxim´ aln´ı unifik´ ator Rezoluˇ cn´ı algoritmus
Pˇr´ıklad Resoluˇcn´ım algoritmem rozhodnˇete, zda plat´ı {∀x.∀y .((P(x) ∧ Q(x, y )) ⇒ R(y )), ∀x.Q(f (x), g (x)), P(f (a))} |= R(g (a)) (Samozˇrejmˇe: popiˇste jazyk PL, ve kter´em jde o sentence.)
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce v PL
16/16
