Rezolúció

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.

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\lor C$ és a $B\lor \lnot C$ formuláknak az $A\lor B$ formula egy logikai következménye, azaz (tétel:)

[(A\lor C)\wedge (B\lor \lnot C)]\rightarrow (A\lor 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, hogyha 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\lor C)\land (h\lor \lnot C)\equiv h\lor (C\land \lnot C)\equiv 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.

Nulladrendű rezolúció

A nulladrendű rezolvens

Legyen

$K:=K_{1}\lor K_{2}\lor ...\lor K_{n}$ és
$L:=L_{1}\lor L_{2}\lor ...\lor 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áljainak nevezzük. 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 (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'\lor \lnot A$
$L:=L'\lor 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)\models K'\lor 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, melynek jele 𝔠.

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_{1}:=K_{1,1}\land K_{1,2}\land ...\land K_{1,n}$
$F_{2}:=K_{2,1}\land K_{2,2}\land ...\land 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}\land K_{1,2}\land ...\land K_{1,n},K_{2,1}\land K_{2,2}\land ...\land K_{2,n}}$ halmazt. 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.

Rezolúció a propozicionális logikában

Elsőrendű rezolúció

Az elsőrendű logikai rezolúció a következtetést egyetlen szabállyá egyszerűsíti le. A megértéséhez a következő példa segít:

Minden görög európai.

Homérosz görög.

Tehát Homérosz európai.

Formálisan ez a következőket jelenti: $\forall X,P(X)\supset Q(X);P(a)\rightarrow Q(a)$ . Rezolúciót alkalmazva először is konjunktív normálformára kell alakítani a premisszákat. Ekkor minden kvantor impliciten a következő módon alakul át:

Univerzális kvantor: kihagyásra kerülnek, az általánosítás szabálya értelmében
Egzisztenciális kvantor: Skolem-függvény helyettesíti őket.

Ilyen formán a következő módon fog kinézni az eredeti levezetésünk: $\lnot P(X)\lor Q(X);P(a)\rightarrow Q(a)$ .

Levezetési technika

A levezetés a következő lépésekkel történik:

Keresünk két, azonos predikátumot ellentétesen negálva tartalmazó klózt
Megkíséreljük egyesíteni, összevonni őket. (Ha nem sikerül, másik két klózt kell választanunk)
Ha nyitott változót tartalmaz az egyik klóz, mely a másikban kötöttként fordul elő, helyettesítsük a kötött termjükkel őket is
Egyszerűsítsünk az összevont predikátumokkal, és kombináljuk a megmaradt kettőt egy új klózzá, diszjunkció segítségével

Példa a levezetésre

Az eredeti példánál maradva: $\lnot P(X)$ előfordul az első klózunkban, míg $P(a)$ megjelenik a második állításunkban. X nem kötött változó, viszont "a" egy kötött atom. Felírható a következő helyettesítés: $X\rightarrow a$ . Megválva az így egyesített predikátumainktól, és a helyettesítést alkalmazva felírható a következtetés: $Q(a)$ .

Források