Rezolúció

A Wikipédiából, a szabad enciklopédiából

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[szerkesztés | forrásszöveg szerkesztése]

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, 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 \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ó[szerkesztés | forrásszöveg szerkesztése]

A nulladrendű rezolvens[szerkesztés | forrásszöveg szerkesztése]

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[szerkesztés | forrásszöveg szerkesztése]

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 Ki,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 propozícionális logikában[szerkesztés | forrásszöveg szerkesztése]

Elsőrendű rezolúció[szerkesztés | forrásszöveg szerkesztése]

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:

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[szerkesztés | forrásszöveg szerkesztése]

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[szerkesztés | forrásszöveg szerkesztése]

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[szerkesztés | forrásszöveg szerkesztése]