Rezoluce v predikátové logice

Rezolu�_ní pravidlo
Máme dv�_ predikátové klauzule (tj. dv�_ disjunkce atomických nebo negovaných atomických formulí). Ozna�_me je L₁ ∨ ... ∨ L_k, M₁ ∨ ... ∨ M_n. Platí-li pro (predikátové) literály L_i a M_j z t�_chto klauzulí a n�_jakou substituci θ ekvivalence L_iθ ≡ ¬M_jθ, můžeme aplikovat následující rezolu�_ní pravidlo:

L₁ ∨ ... ∨ L_k M₁ ∨ ... ∨ M_n

(L₁ ∨ ... ∨ L_i-1 ∨ L_i+1 ∨ ... ∨ L_k ∨ M₁ ∨ ... ∨ M_j-1 ∨ M_j+1 ∨ ... ∨ M_n)θ

Substituce θ se nazývá unifikace. Unifikací můžeme najít vícero, zajímají nás ale ty nejobecn�_jší (tzv. most general unifier - mgu), tedy takové unifikace θ, že pro každou unifikaci ξ existuje substituce η, že ξ = θη. S nejobecn�_jšími unifikacemi po�_ítáme proto, aby záv�_r pravidla byl co nejobecn�_jší.

P�_íklad

P(f(x)) ∨ Q(g(x),x) ¬Q(u,v) ∨ ¬R(u,v)

P(f(x)) ∨ ¬R(g(x),x)

kde byla použita mgu θ={u/g(x), v/x}.

Rezoluce je posloupnost rezolu�_ních pravidel, která aplikujeme na po�_áte�_ní množinu klauzulí i na výsledky p�_edchozích rezolu�_ních pravidel.
Chceme-li zjistit, jestli lze z množiny formulí Γ odvodit formule φ, postupujeme bu�_ dop�_edn�_ (takto fungují produk�_ní systémy, DATALOG), nebo zp�_tn�_ (nap�_. PROLOG). Dop�_edná metoda vezme množinu Γ a aplikuje na ni rezoluci tak dlouho, dokud není odvozena φ nebo dokud nemáme odvozenu množinu všech teorémů. Metoda zp�_tná aplikuje rezoluci na množinu Γ∪{¬φ}, p�_i�_emž první použité pravidlo má jako jeden z p�_edpokladů ¬φ. Cílem je dojít k prázdné klauzuli, která indikuje spornost množiny Γ∪{¬φ}, a tedy odvoditelnost φ z Γ.

Podrobn�_jší informace o rezoluci a unifika�_ním algoritmu zazn�_ly v p�_ednášce a jsou obsaženy na stránkách University of Miami. Upozor�_uji, že tam používají trochu jiné zna�_ení (nap�_. výrokovou spojku ∨ zna�_í |).