Rezolúció

A Wikipédiából, a szabad lexikonból.

Tartalomjegyzék 1 A rezolúciós kalkulus alaptétele 2 Nulladrendű rezolúció 2.1 A nulladrendű rezolvens 2.2 A rezolúciós eljárás vázlatos menete

A rezolúció a matematikai logikában egy levezetési eljárás, mely alapja az egyik automatikus tételbizonyítási módszernek, elméletnek, a rezolúciós kalkulusnak. Az eljárás az informatikában is jelentős, mivel a logikai programozás alapnyelve, a Prolog a rezolúció egy fajtájának, az elsőrendű lineáris rezolúciónak az algoritmikus megvalósítása.

A rezolúció szintaktikus módszer (az eljárás kiinduló formuláinak alakja, felépítése alapján működik); alapja, hogy két logikai formulához hozzárendeljük egy speciális következményformulájukat, az ún. rezolvensüket.

A rezolválandó formulákat először konjunktív normálforma alakúra kell hozni. Erre létezik automatikus eljárás; bár a logikai programozási nyelvek általában már feltételezik, hogy ez megtörtént, és csak speciális alakú formulákkal (ún. programklózok) tudnak dolgozni.

[szerkesztés] A rezolúciós kalkulus alaptétele

A rezolúciós kalkulus alapjául a következő elemi logikai tétel szolgál:

Legyenek A,B,C tetszőleges (nulladrendű) formulák, ekkor az A∨C és a B∨¬C formuláknak az A∨B formula egy logikai következménye, azaz (tétel:)

[(A∨C)∧(B∨¬C)] ⇒ (A∨B)

Ez értéktáblázattal, de anélkül is belátható. A ⇒ operátor definíciója alapján ez egy akkor érvényes következtetésmód, hogy ha az előtag igaz, akkor az utótag is, azaz; a következtetésmód akkor és csak akkor hamis, ha az előtag igaz, de az utótag hamis. Utóbbi pedig nem lehetséges, mert ha az utótag hamis, akkor lévén A és B diszjunkciója, ennek mindkét tagja is hamis kell hogy legyen, tehát A is és B is hamis. Ez esetben az előtag (h∨C)∧(h∨¬C) ≡ h∨(C∧¬C) ≡ h, tehát ez esetben az előtag azonosan hamis, így a következtetésmód mint formula, minden interpretációban igaz, egyszóval érvényes.

[szerkesztés] Nulladrendű rezolúció

[szerkesztés] A nulladrendű rezolvens

Legyen

• K := K₁∨K₂∨...∨K_n és
• L := L₁∨L₂∨...∨L_m (n,m>0)
  két nulladrendű klóz (azaz negált vagy negálatlan atomi formulák diszjunkciója). Az egyes negált vagy negálatlan atomi formulákat (K_i, L_j) a klózok literálainak nevezzük. Mármost ha van a K, L formulákban egy-egy olyan literál, amely azonos atomból áll, de K-ban ellenkezőképp negált, mint L-ben (azaz K-ban negálatlan, de L-ben negált, vagy fordítva); akkor a K,L klózpárt rezolválhatónak mondjuk, ekkor tehát (az általánosság megszorítása nélkül feltételezve, hogy ez az atom mondjuk A, és K-ban negált, L-ben negálatlan) K és L a következőképp írható:
• K := K'∨¬A
• L := L'∨A

ahol K', L' szintén klózok, literálok diszjunkciói; ez esetben K és L nulladrendű rezolvense a következő klóz: (K,L) := K'∨L'

Összefoglalva megállapíthatjuk, hogy ha van két olyan klózunk, melyek tartalmaznak egy-egy ellenkezően negált, de azonos (atom)alapú literált, akkor (és csak akkor) a rezolvensképzés lehetséges, és abban áll, hogy e két ellenkezően negált literált „kiejtve”, a maradék literálokat egyetlen klózzá egyesítjük (összediszjunkciózzuk).

Ha K' és L' üres diszjunkció, akkor azt mondjuk, hogy a rezolvens az űres klóz.

[szerkesztés] A rezolúciós eljárás vázlatos menete

A nulladrendű logikai nyelvek két rezolválandó formuláját hozzuk először konjunktív normálforma alakra:

• F₁ := K_1,1 ∧ K_1,2 ∧ ... ∧ K_1,n
• F₂ := K_2,1 ∧ K_2,2 ∧ ... ∧ K_2,n

ahol K_i,j a konjunktív normálforma alakú formulák klózai.

Képezzük az összes klózból álló G := {K_1,1 ∧ K_1,2 ∧ ... and; K_1,n, K_2,1 ∧ K_2,2 ∧ ... and; K_2,n}. Az eljárás alapja, hogy minden lépésben kiválasztunk két klózt, és képezzük azok ún. nulladrendű rezolvensét (ez is egy speciális konjunktív normálformula, mégpedig egy klóz), majd ezt a kapott formulát visszahelyezzük a G klózhalmazba.

Az eljárást addig folytatjuk, amíg elfogynak a rezolválható klózok (nem maradnak már kirezolválható literálok), ebben az esetben az eljárás sikertelen; vagy amíg „le nem vezetjük az üres klózt” (ez esetben az eljárás sikeres).

Ez így ebben a formában láthatóan nem algoritmus, hanem indeterminisztikus eljárás. A rezolúció „kevésbé determinisztikussá” alakításával (erre szolgálnak a rezolúciólinearizálás illetve az inputrezolúció és hasonló eljárások) és eme némileg csökkent többértelműségű eljáráscsaládok algoritmussá alakításával (ld. LUSH) lehetséges a determinisztikussá tétel, s ezáltal a gépi megvalósítás.