Rezolúció

A Wikipédiából, a szabad enciklopédiából
Ugrás a navigációhoz Ugrás a kereséshez

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]

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

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

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 , 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]

A nulladrendű rezolvens[szerkesztés]

Legyen

  • és

  • 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 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ó:

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

Ö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]

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

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

Képezzük az összes klózból álló 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[szerkesztés]

Elsőrendű rezolúció[szerkesztés]

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: . 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: .

Levezetési technika[szerkesztés]

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]

Az eredeti példánál maradva: előfordul az első klózunkban, míg 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: . Megválva az így egyesített predikátumainktól, és a helyettesítést alkalmazva felírható a következtetés: .

Források[szerkesztés]