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

$[(A\vee C)\wedge (B\vee \mathrm{\neg }C)]\to (A\vee 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\vee C)\wedge (h\vee \mathrm{\neg }C)\equiv h\vee (C\wedge \mathrm{\neg }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\vee K_2\vee ...\vee K_n$ és
• $L:=L_1\vee L_2\vee ...\vee 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^{\prime }\vee \mathrm{\neg }A$
• $L:=L^{\prime }\vee 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^{\prime }\vee L^{\prime }$

Ö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}\wedge K_{1,2}\wedge ...\wedge K_{1,n}$
• $F_2:=K_{2,1}\wedge K_{2,2}\wedge ...\wedge 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}\wedge K_{1,2}\wedge ...\wedge K_{1,n},K_{2,1}\wedge K_{2,2}\wedge ...\wedge 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.

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: $\mathrm{\forall }X,P(X)\supset Q(X);P(a)\to 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: $\mathrm{\neg }P(X)\vee Q(X);P(a)\to 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: $\mathrm{\neg }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\to 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

• Várterész Magda - Mesterséges Intelligencia 2, Debreceni Egyetem
• Rezolúció
• Takács Márta - Logika 4