Klaus´ aln´ı tvar mnoˇ ziny formul´ı Rezolventy Rezoluˇ cn´ı algoritmus
Rezoluce ve v´ yrokov´ e logice
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce ve VL
1/13
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Rezolventy Rezoluˇ cn´ı algoritmus
Z´ akladn´ı myˇslenky 1
M |= ϕ iff X = M ∪ {¬ϕ} nesplniteln´a.
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.
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce ve VL
2/13
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Rezolventy Rezoluˇ cn´ı algoritmus
CNF — Pˇripomenut´ı (viz cviˇ cen´ı) ˇ At’ ϕ je formule VL. Rekneme, ˇze ψ je CNF pro ϕ, kdyˇz je 1
ϕ |=| ψ
2
ψ je bud’ tt nebo koneˇcn´a konjunkce ψ1 ∧ . . . ∧ ψn
3
Kaˇzd´emu ψi ˇr´ık´ame klausule (pro CNF) a m´a tvar bud’ ff nebo `1 ∨ . . . ∨ `ki . Kaˇzd´emu `j ˇr´ık´ame liter´al: je to bud’ atom nebo negace atomu.
4
CNF v BNF ,
` ::= a | ¬a ψ ::= ff | (ψ ∨ `) ϕ ::= tt | (ϕ ∧ ψ)
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce ve VL
3/13
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Rezolventy Rezoluˇ cn´ı algoritmus
Jak naj´ıt CNF? 1
Karnaughova mapa (cviˇcen´ı).
2
Syntakticky: pˇrepisovac´ı pravidla (cviˇcen´ı).
3
A jin´e metody: napˇr´ıklad algoritmus Quine–McCluskey (nebudeme uv´adˇet), je ale hodnˇe podobn´y metodˇe Karnaughov´ych map.
Viz http://www.ee.surrey.ac.uk/Projects/Labview/minimisation/tabular.h
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce ve VL
4/13
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Rezolventy Rezoluˇ cn´ı algoritmus
Klaus´ aln´ı tvar ˇ At’ X je mnoˇzina formul´ı VL. Rekneme, ˇze kt(X ) je klaus´aln´ı tvar mnoˇziny X , pokud plat´ı: α ∈ kt(X ) iff α je klausule pro CNF nˇejak´e formule z X . Pˇr´ıklad: Klaus´ aln´ı tvar nen´ı urˇ cen jednoznaˇ cnˇ e! At’ a, b, c ∈ At. X = {a ⇒ (b ∨ c), (b ∨ c) ∧ (b ∨ ¬c)}. CNF jednotliv´ych formul´ı: ¬a ∨ b ∨ c a (b ∨ c) ∧ (b ∨ ¬c). Pˇr´ısluˇsn´e kt(X ) je mnoˇzina {¬a ∨ b ∨ c, b ∨ c, b ∨ ¬c}. Jin´a moˇznost: druhou formuli v mnoˇzinˇe X upravit na synonymum b. Pˇr´ısluˇsn´e kt(X ) je mnoˇzina {¬a ∨ b ∨ c, b}.
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce ve VL
5/13
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Rezolventy Rezoluˇ cn´ı algoritmus
Definice Mnoˇziny A a B formul´ı VL jsou ekvisplniteln´e, kdyˇz A a B jsou bud’ obˇe souˇcasnˇe splniteln´e nebo jsou A a B obˇe souˇcasnˇe nesplniteln´e. Pozorov´ an´ı X a kt(X ) jsou ekvisplniteln´e. D˚ usledek Staˇc´ı se zamˇeˇrit na kritick´e“ d˚ usledky kt(X ). ”
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce ve VL
6/13
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Rezolventy Rezoluˇ cn´ı algoritmus
Definice Dvˇe klausule α1 a α2 maj´ı komplement´arn´ı v´yskyt atomick´e formule a, kdyˇz bud’ α1 obsahuje liter´al a a α2 obsahuje liter´al ¬a nebo naopak. Definice At’ α1 a α2 jsou dvˇe klausule s komplement´arn´ım v´yskytem atomick´e formule a. Jako resa (α1 , α2 ) (ˇcteme: resolventa klausul´ı α1 , α2 podle a) oznaˇc´ıme klausuli, kter´a obsahuje vˇsechny liter´aly obsaˇzen´e v α1 a α2 kromˇe liter´al˚ u a a ¬a.
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce ve VL
7/13
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Rezolventy Rezoluˇ cn´ı algoritmus
Pˇr´ıklad At’ a, b, c ∈ At. 1
resb (a ∨ ¬b ∨ c, a ∨ b ∨ c) = a ∨ c
2
resb (a ∨ ¬b ∨ c, a ∨ b ∨ ¬c) = a ∨ c ∨ ¬c
3
resc (a ∨ ¬b ∨ c, a ∨ b ∨ ¬c) = a ∨ ¬b ∨ b
4
resa (a, ¬a) = ff
5
resa (a, a ∨ b) neexistuje
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce ve VL
8/13
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Rezolventy Rezoluˇ cn´ı algoritmus
Vˇ eta At’ α1 a α2 jsou dvˇe klausule s komplement´arn´ım v´yskytem atomick´e formule a. Potom jsou mnoˇziny {α1 , α2 } a {α1 , α2 , resa (α1 , α2 )} ekvisplniteln´e.a a
V m´ych skriptech (Tvrzen´ı 4.1.9, str. 54) je chyba, opravte si ji.
D˚ usledek At’ α1 a α2 jsou dvˇe klausule s komplement´arn´ım v´yskytem atomick´e formule a. Potom plat´ı {α1 , α2 } |= resa (α1 , α2 ).
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce ve VL
9/13
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Rezolventy 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 ve VL
10/13
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Rezolventy 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 ve VL
11/13
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Rezolventy 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 (resoluˇcn´ı tabulku) naleznete ve skriptu M. Demlov´a a B. Pondˇel´ıˇcek, Matematick´a logika, FEL ˇ CVUT, Praha 1997 Resoluˇcn´ı tabulka vˇsak nen´ı pravdivostn´ı tabulka! Tvorba resoluˇcn´ı tabulky je opˇet syntaktick´y algoritmus.
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce ve VL
12/13
Klaus´ aln´ı tvar mnoˇ ziny formul´ı Rezolventy Rezoluˇ cn´ı algoritmus
Pˇr´ıklady Rozhodnˇete o splnitelnosti tvorbou resoluˇcn´ı tabulky: 1
{x ∨ y ∨ ¬z, ¬x, x ∨ y ∨ z, x ∨ ¬y , z ∨ t ∨ v , ¬t ∨ w }, kde x, y , z, t, v , w ∈ At.
2
{a ∨ ¬d, ¬b ∨ ¬c, b ∨ d, ¬b ∨ ¬e, a ∨ c ∨ d, ¬a ∨ ¬d}, kde a, b, c, d, e ∈ At.
Jiˇr´ı Velebil: AD0B01LGR 2015
Rezoluce ve VL
13/13
