Mint az ítélatlogika esetében, az elsőrendű rezolúció is megköveteli, hogy a mondatok konjunktív normál formában (conjunctive normal form) (CNF) legyenek, tehát minden mondat klózok konjunkciója, ahol minden egyes klózt literálok diszjunkciója alkot.^[92] A literálok tartalmazhatnak változókat, amelyeket univerzális kvantorral ellátottnak feltételezünk. Például a

∀x Amerikai(x) ∧ Fegyver(y) ∧ Elad(x, y, z) ∧ Ellenséges(z) ⇒ Bűnöző(x)

mondat CNF-formára átalakítva ilyen lesz:

¬Amerikai(x) ∨ ¬Fegyver(y) ∨ ¬Elad(x, y, z) ∨ ¬Ellenséges(z) ∨ Bűnöző(x)

A CNF-mondatok átalakításának eljárása nagyon hasonló az ítéletlogikai eljáráshoz, amelyet a „Konjunktív normál forma”részben láthatunk. A legfontosabb különbség abból fakad, hogy ki kell vonnunk a mondatokból az egzisztenciális kvantorokat. Ezt az eljárást a következő mondat lefordításával illusztráljuk: „Mindenkit, aki az összes állatot szereti, valaki szeret”, vagyis:

∀x [∀y Állat(y) ⇒ Szereti(x, y)] ⇒ [∃y Szereti(y, x)]

A lépések a következők:

∀x [¬∀y ¬Állat(y) ∨ Szereti(x, y)] ∨ [∃y Szereti(y, x)]

¬∀x p-ből lesz ∃x ¬p

¬∃x p-ből lesz ∀x ¬p

A mondatunk a következő átalakításokon megy keresztül:

∀x [∃y ¬(¬Állat(y) ∨ Szereti(x, y))] ∨ [∃y Szereti(y, x)]

∀x [∃y ¬ ¬Állat(y) ∧ ¬Szereti(x, y)] ∨ [∃y Szereti(y, x)]

∀x [∃y Állat(y) ∧ ¬Szereti(x, y)] ∨ [∃y Szereti(y, x)]

Figyeljük meg, hogyan alakítottuk át az univerzális kvantort (∀y) az implikáció premisszájában egzisztenciális kvantorrá. A mondatot most így lehet kiolvasni „Vagy van olyan állat, amelyet x nem szeret, vagy (ha ez nem áll fenn) valaki szereti x-et.” Világos, hogy az eredeti mondat jelentését megőriztük.

∀x [∃y Állat(y) ∧ ¬Szereti(x, y)] ∨ [∃z Szereti(z, x)]

∀x [Állat(A) ∧ ¬Szereti(x, A)] ∨ Szereti(B, x)

amelynek teljesen téves a jelentése: azt mondja ki, hogy mindenki vagy nem tud szeretni egy bizonyos A állatot, vagy egy bizonyos B entitás szereti őt. Valójában, az eredeti mondatunk lehetővé teszi minden egyes személy számára, hogy ne szeressen egy másik állatot, vagy egy másik személy szeresse őt. Így tehát, azt szeretnénk, hogy a Skolem entitások az x-től függjenek:

∀x [Állat(F(x)) ∧ ¬Szereti(x, F(x))] ∨ Szereti(G(x), x)

Itt az F és a G Skolem-függvények. Az általános szabály az, hogy a Skolem-függvények argumentumai mind univerzális kvantorral ellátott változók, amelyeknek a hatókörében az egzisztenciális kvantor értelmezett. Hasonlóan az Egzisztenciális Példányosításhoz, a skolemizált mondat is pontosan akkor kielégíthető, ha az eredeti mondat is kielégíthető.

[Állat(F(x)) ∧ ¬Szereti(x, F(x))] ∨ Szereti(G(x), x)

[Állat(F(x)) ∨ Szereti(G(x), x)] ∧ [ ¬Szereti(x, F(x)) ∨ Szereti(G(x), x)]

Ennek a lépésnek az elvégzéséhez szükség lehet az egymásba ágyazott konjunkciók és diszjunkciók kibontására is.

A mondat most CNF formájú, és két klózból áll. Eléggé olvashatatlan lett. (Némiképpen segíthet, ha megmagyarázzuk, hogy az F(x) függvény egy, az x személy által potenciálisan nem szeretett állatra vonatkozik, míg a G(x) olyan valakire utal, aki szeretheti x-et.) Szerencsére, nekünk ritkán kell CNF-mondatokat vizsgálnunk – a fordítási folyamat könnyen automatizálható.

Az elsőrendű klózokra vonatkozó következtetési szabály egyszerűen a 7.5.1. szakasz - Rezolúció részben megadott propozíciós rezolúciós szabály kiterjesztett változata. Két klóz, amelyek standardizálva vannak, tehát nem tartalmaznak azonos változókat, akkor rezolválható, ha tartalmaznak komplememens literálokat. Az ítéletlogikai literálok akkor komplemensek, ha az egyik a negációja a másiknak; míg az elsőrendű literálok akkor komplemensek, ha az egyik egyesül a másik negációjával. Így ezt kapjuk:

ahol az EGYESÍT (l_i, ¬m_j) = θ. Például rezolválhatjuk ezt a két klózt:

[Állat(F(x)) ∨ Szereti(G(x), (x)] és [¬Szereti(u, v) ∨ ¬Megöli(u, v)]

a θ = {u/G(x), v/x} egyesítő felhasználásával a komplemens literálokat, a Szereti(G(x), x)-t és a ¬Szereti(u, v)-t eliminálva kapjuk meg a rezolvens (resolvent) klózt:

[Állat(F(x)) ∨ ¬Megöli(G(x), x)]

A bemutatott szabály neve bináris rezolúciós (binary resolution) szabály, mert pontosan két literált old fel. A bináris rezolúciós szabály önmagában nem eredményez egy teljes következtetési folyamatot. A teljes rezolúciós szabály literálok részhalmazait rezolválja minden egyes egyesíthető klózban. Egy alternatív megközelítés a faktorálásnak (factoring), a felesleges literálok eltávolításának a kiterjesztése az elsőrendű logikára. A propozíciós faktorálás két literált eggyé redukál, ha azok azonosak. Az elsőrendű faktorálás két literált eggyé redukál, ha azok egyesíthetők. Az egyesítőt a teljes klózra kell alkalmazni. A bináris rezolúció és a faktorálás kombinációja már teljes eljárást eredményez.

A rezolúció a TB ⊨ α állítást úgy igazolja, hogy bebizonyítja, hogy a TB ∧ ¬α nem kielégíthető, vagyis a bizonyítás az üres klóz származtatásával történik. Az algoritmikus megközelítés megegyezik az ítéletlogikában lévővel, amelyet a 7.12. ábrán már bemutattunk, így ezt itt most nem ismételjük meg. Ehelyett inkább két példabizonyítást adunk meg. Az első a bűntény példa a 9.3. alfejezetből. A mondatok CNF-ben a következők:

¬Amerikai(x) ∨ ¬Fegyver(y) ∨ ¬Elad(x, z, y) ∨ ¬Ellenséges(z) ∨ Bűnöző(x)

¬Rakéta(x) ∨ ¬Birtokol(Nono, x) ∨ Elad(West, x, Nono)

¬Ellenség(x, Amerika) ∨ Ellenséges(x)

¬Rakéta(x) ∨ Fegyver(x)

Birtokol(Nono, M1) Rakéta(M1)

Amerikai(West) Ellenség(Nono, Amerika)

Hozzáadjuk a mondatok halmazához a negált célt is ¬Bűnöző(West). A rezolúciós bizonyítást a 9.11. ábra mutatja be. Figyeljük meg a szerkezetét: a bizonyításnak egy egyszerű „gerince” van, amely a célklózzal kezdődik, és folyamatosan rezolvál a tudásbázisból származó klózokkal, mindaddig, amíg az üres klózt nem generálja. Ez jellemző a Horn-klózokat tartalmazó tudásbázisokon végzett rezolúcióra. Valójában a fő gerinc mentén található klózok pontosan megfelelnek a 9.6. ábrán látható hátrafelé láncolási algoritmusban a célváltozók egymást követő értékeinek. Ez azért van így, mert mindig azt a klózt választjuk ki rezolválásra, amelynek a pozitív literálja egyesíthető a gerincen lévő „aktuális” klóz bal szélen elhelyezkedő literáljával, és pontosan ez történik a hátrafelé láncolásban is. Így tehát a hátrafelé láncolás valójában a rezolúció egy speciális esete, egy különleges vezérlési stratégiával, amely meghatározza, hogy melyik rezolúciót hajtsuk végre legközelebb.

A második példánk kihasználja a skolemizációt, és nem határozott klózokat is tartalmaz. Ez valamivel bonyolultabb bizonyítási struktúrát eredményez. Természetes nyelven megfogalmazva a probléma a következő:

Mindenkit, aki az összes állatot szereti, szeret valaki.

Bárkit, aki megöl egy állatot, senki sem szeret.

Jankó szereti az összes állatot.

Vagy Jankó, vagy a Kíváncsiság ölte meg a macskát, akinek a neve Tuna.

A Kíváncsiság ölte meg a macskát?

Először is leírjuk az eredeti mondatokat, némi háttértudást, és a G negált célt az elsőrendű logikában:

A. ∀x [∀y Állat(y) ⇒ Szereti(x, y)] ⇒ [∃y Szereti(y, x)]

B. ∀x [∃y Állat(y) ∧ Megöli(x, y)] ⇒ [∀z ¬Szereti(z, x)]

C. ∀x Állat(x) ⇒ Szereti(Jankó, x)

D. Megöli(Jankó, Tuna) ∨ Megöli(Kíváncsiság, Tuna)

E. Macska(Tuna)

F. ∀x Macska(x) ⇒ Állat(x)

G. ¬Megöli(Kíváncsiság, Tuna)

Most pedig alkalmazzuk az átalakítási procedúrát, hogy minden egyes mondatot CNF-be konvertáljunk:

A1. Állat(F(x)) ∨ Szereti(G(x), x)

A2. ¬Szereti(x, F(x)) ∨ Szereti(G(x), x)

B. ¬Állat(y) ∨ ¬Megöli(x, y) ∨ ¬Szereti(z, x)

C. ¬Állat(x) ∨ Szereti(Jankó, x)

D. Megöli(Jankó, Tuna) ∨ Megöli(Kíváncsiság, Tuna)

E. Macska(Tuna)

F. ¬Macska(x) ∨ Állat(x)

¬G. ¬Megöli(Kíváncsiság, Tuna)

A 9.12. ábrán látható a rezolúciós bizonyítása annak, hogy a Kíváncsiság ölte meg a macskát. Magyarul a bizonyítást így írhatjuk át:

Tegyük fel, hogy a Kíváncsiság nem ölte meg Tunát. Tudjuk, hogy vagy Jankó, vagy a Kíváncsiság tette; tehát biztosan Jankó tehette. Mármost, Tuna egy macska, és a macskák állatok, tehát Tuna egy állat. Mivel bárkit, aki megöl egy állatot, senki sem szeret, tudjuk, hogy Jankót nem szereti senki. Másrészt, Jankó minden állatot szeret, tehát valaki szereti őt, tehát ez az ellentmondás áll fenn. Így tehát a Kíváncsiság ölte meg a macskát.

A bizonyítás képes megválaszolni a „A Kíváncsiság ölte meg a macskát?” kérdést, de gyakran ennél általánosabb kérdéseket akarunk feltenni, mint például: „Ki ölte meg a macskát?” A rezolúció meg tudja válaszolni ezt is, de ennek a válasznak a levezetése egy kicsit több munkát igényel. A célállítás a ∃w Megöli(w, Tuna), amely negáláskor CNF-ben ¬Megöli(w, Tuna) lesz. Megismételve a bizonyítást a 9.12. ábrán az új negált céllal, hasonló bizonyítási fát kapunk, de a következő helyettesítéssel: {w/Kíváncsiság} az egyik lépésben. Így ebben az esetben, annak a kiderítése, hogy ki ölte meg a macskát, nem áll másból, mint a lekérdezés változóiban lévő lekötések nyomon követése a bizonyításban.

Sajnos, a rezolúció csak nem konstruktív bizonyítást (nonconstructive proofs) tud előállítani az egzisztenciális célmondatokra. Például a ¬Megöli(w, Tuna) rezolválható a Megöli(Jankó, Tuna) ∨ Megöli(Kíváncsiság, Tuna)-val, hogy a Megöli(Jankó, Tuna) mondatot megkapjuk, amely megint rezolválható ezzel: ¬Megöli(w, Tuna), és így kapjuk meg az üres klózt. Figyeljük meg, hogy ebben a bizonyításban a w-nek két különböző lekötése van. A rezolúció megmutatja azt, hogy igen, valaki megölte Tunát – vagy Jankó, vagy a Kíváncsiság. Ez nem túl meglepő! Egy lehetséges megoldás korlátozni a rezolúciós lépéseket úgy, hogy a kérdés változóinak csak egy lekötésük lehessen egy adott bizonyításban, majd képesnek kell lennünk arra, hogy visszakövessük a lehetséges lekötéseket. Egy másik megoldás egy speciális válasz literál (answer literal) hozzáadása a negált célhoz, amelyből ez lesz: ¬Megöli(w, Tuna) ∨ Válasz(w). Ilyenkor a rezolúciós folyamat mindig generál egy pontosan egy literált tartalmazó választ, amikor egy ilyan klóz generálódik. A 9.12. ábrán látható bizonyításra ez a Válasz(Kíváncsiság).A nem konstruktív bizonyítás ezt a klózt generálná: Válasz(Kíváncsiság) ∨ Válasz(Jankó), amely nem ad számunkra választ.

Ebben a részben bebizonyítjuk a rezolúció teljességét. A fejezet elolvasását nyugodtan kihagyhatja bárki, aki megelégszik azzal, hogy elhiszi ezt az állítást.

Be fogjuk mutatni, hogy a rezolúció cáfolásteljes (refutation-complete), ami azt jelenti, hogy ha egy mondathalmaz kielégíthetetlen, akkor a rezolúció mindig képes levezetni egy ellentmondást. A rezolúció nem alkalmazható arra, hogy mondatok egy halmazának összes logikai következményét generálja, de használható arra, hogy megmondjuk, hogy egy adott mondat következménye-e a mondathalmaznak. Így alkalmazható egy adott kérdésre adható összes válasz megtalálására, felhasználva a korábban a fejezetben már bemutatott célnegálás módszert.

Bizonyításunk váza követi Robinson eredeti bizonyítását, néhány Geneserethtől és Nilssontól származó egyszerűsítés hozzáadásával (Genesereth és Nilsson, 1987). A 9.13. ábra mutatja be a bizonyítás alapvető struktúráját, ami a következő:

Az első lépés elvégzéséhez szükségünk lesz három új fogalomra:

Például, ha az S csak a ¬P(x, F(x, A)) ∧ ¬Q(x, A) ∨ R(x, B) klózt tartalmazza, akkor a H_S az alapmondatok következő végtelen halmaza:

{A, B, F(A, A), F(A, B), F(B, A), F(B, B), F(A, F(A, A)), …}

{¬P(A, F(A, A)) ∨ ¬Q(A, A) ∨ R(A, B),

¬P(B, F(B, A)) ∨ ¬Q(B, A) ∨ R(B, B),

¬P(F(A, A), F(F(A, A), A)) ∨ ¬Q(F(A, A), A) ∨ R(F(A, A), B)

¬P(F(A, B), F(F(A, B), A)) ∨ ¬Q(F(A, B), A) ∨ R(F(A, B), B), …}

Ezek a definíciók lehetővé teszik, hogy a Herbrand-tétel (Herbrand’s theorem) egyik formáját állítsuk:

Legyen S′ ez a véges részhalmaza az alapmondatoknak. Mármost, alkalmazhatjuk az alap rezolúciós tételt („A rezolúció teljessége” részben), hogy kimutassuk, hogy a rezolúciós! lezárt (resolution! closure) RC(S′) tartalmazza az üres klózt. Ez azt jelenti, hogy a propozíciós rezolúció futtatása a teljességig az S′-en egy ellentmondást fog eredményezni.

Most, hogy megállapítottuk, hogy mindig van egy rezolúciós bizonyítás, amely magában foglal néhány véges részhalmazt a Herbrand S bázisból, a következő lépés annak megmutatása, hogy létezik egy rezolúciós bizonyítás, amely magának az S-nek a klózait tartalmazza, amelyek nem szükségszerűen alapklózok. Azzal kezdjük, hogy megvizsgáljuk a rezolúciós szabály egy egyszerű alkalmazását. Robinson alaplemmája magába foglalja a következő tényt:

Legyen C₁ és C₂ két klóz, amelyeknek nincsenek közös változói. Legyenek C₁′ és C₂′ az alappéldányai C₁-nek és C₂-nek. Ha C′ rezolvense C₁′-nek és C₂′-nek, akkor létezik egy olyan C klóz, amelyik (1) rezolvense C₁-nek és C₂-nek és (2) C′ alappéldánya C-nek.

Ezt kiterjesztéslemmának (lifting lemma) nevezik, mivel kiterjeszti a bizonyítási lépést az alap klózokról az általános elsőrendű klózokra. A kiterjesztési lemma bizonyításához Robinsonnak szüksége volt az egyesítés módszerének megalkotására és a legáltalánosabb egyesítő tulajdonságainak levezetésére is. A bizonyítás áttekintése helyett a következőkben illusztráljuk a lemmát:

C1 = ¬P(x, F(x, A)) ∨ ¬Q(x, A) ∨ R(x, B)

C2 = ¬N(G(y), z)) ∨ P(H(y), z)

C'1 = ¬P(H(B), F(H(B), A)) ∨ ¬Q(H(B), A) ∨ R(H(B), B)

C'2 = ¬N(G(B), F(H(B), A)) ∨ P(H(B), F(H(B), A))

C' = ¬N(G(B), F(H(B), A)) ∨ ¬Q(H(B), A) ∨ R(H(B), B)

C = ¬N(G(y), F(H(y), A)) ∨ ¬Q(H(y), A) ∨ R(H(y), B)

Látható, hogy C′ valóban C alaptermje. Általánosságban ahhoz, hogy C₁′-nek és C₂′-nek legyen rezolvense, úgy kell létrehozni őket, hogy először a C₁-beli és a C₂-beli komplemens literálok legáltalánosabb egyesítőjét alkalmazzuk C₁-re és C₂-re. A kiterjesztési lemma felhasználásával könnyű hasonló állításokat levezetni a rezolúciós szabály alkalmazásának bármely sorozatára:

Bármely az S′ lezárásához tartozó C′ klózhoz létezik egy S lezárásában levő C klóz, amelyre a C′ klóz a C klóz alappéldánya, és a C levezetése azonos hosszúságú a C′ levezetésével.

Ebből a tényből következik, hogy ha S′ lezárásában megjelenik az üres klóz, akkor ez szintén megtalálható az S rezolúciós lezárásában. Ez azért van, mivel az üres klóz semmilyen más klóznak sem alappéldánya. Összefoglalva: megmutattuk, hogyha S nem kielégíthető, akkor létezik az üres klóznak egy véges méretű rezolúciós szabályt alkalmazó levezetése.

Az elmélet bizonyításában az alapklózokról az elsőrendű klózokra történő kiterjesztés az állítás erejének igen jelentős növelése. Ez abból következik, hogy az elsőrendű bizonyításban már csak annyiszor kell a változókat helyettesíteni, amennyiszer ez a bizonyításhoz szükséges, míg az alapklózmódszereknél szükséges volt nagyszámú önkényes példányosítást megvizsgálni.

Az ebben a fejezetben az eddig leírt következtetési módszerek közül egyik sem foglalkozott az egyenlőséggel. Három jól elkülöníthető megközelítést alkalmazhatunk. Az első az, hogy axiómákkal látjuk el az egyenlőséget – vagyis leírunk mondatokat az egyenlőségi relációról a tudásbázisban. El kell mondanunk, hogy az egyenlőség reflexív, szimmetrikus, tranzitív, és hogy az egyenlők helyettesíthetők egyenlőkkel bármely predikátumban vagy függvényben. Ezért van szükségünk három alapaxiómára, majd ezután egy továbbira minden egyes predikátumhoz vagy függvényhez:

∀x x = x

∀x, y x = y ⇒ y = x

∀x, y, z x = y ∧ y = z ⇒ x = z

∀x, y x = y ⇒ (P1(x) ⇔ P1(y))

∀x, y x = y ⇒ (P2(x) ⇔ P2(y))

.

.

.

∀w, x, y, z w = y ∧ x = z ⇒ (F1(w, x) = F1(y, z))

∀w, x, y, z w = y ∧ x = z ⇒ (F2(w, x) = F2(y, z))

.

.

.

Mikor ezek a mondatok adottak, egy standard következtetési eljárás, mint amilyen a rezolúció elvégezhet olyan feladatokat, amelyek egyenlőségi következtetést igényelnek, mint például a matematikai egyenletek megoldása.

Az egyenlőség kezelésének másik módja egy további következtetési szabály alkalmazása. A legegyszerűbb szabály, a demoduláció (demodulation) vesz egy egységklózt, x = y és helyettesíti az y-t bármely termmel, ami x-szel egyesíthető egy másik klózban. Formálisabban kifejezve ezt kapjuk:

A demodulációt jellemzően arra használják, hogy leegyszerűsítsen állítások kollekcióit használó kifejezéseket, mint például x + 0 = x, x¹ = x és így tovább. A szabályt ki lehet terjeszteni, hogy olyan nem egység klózokkal is tudjon foglalkozni, amelyekben egy egyenlőségi literál megjelenik.

A demodulációval ellentétben a paramoduláció egy teljes következtetési eljárást eredményez az egyenlőséggel rendelkező elsőrendű logikában.

Egy harmadik megközelítés az egyenlőségi következtetést teljes mértékben egy kiterjesztett egyesítési algoritmuson belül kezeli. Ez azt jelenti, hogy a termek egyesíthetők, ha bizonyíthatóan egyenlők egy bizonyos helyettesítés alatt, ahol a „bizonyíthatóan” lehetővé tesz egy bizonyos mennyiségű egyenlőségi következtetést. Például, azok a termek, hogy 1 + 2 és 2 + 1 normális esetben nem egyesíthetők, de egy egyesítési algoritmus, amely ismeri, hogy x + y = y + x, tudná őket egyesíteni az üres helyettesítéssel. Az ilyen fajta egyenleti egyesítés (equational unification) elvégezhető hatékony algoritmusokkal, amelyeket arra terveztek, hogy a felhasznált bizonyos axiómákat használja (kommutativitás, asszociativitás és így tovább), ahelyett hogy explicit következtetéseket tenne ugyanazokkal az axiómákkal. A tételbizonyítások, amelyek ezt a technikát használják, szoros kapcsolatban állnak a korlátozott logikai programozási rendszerekkel, amelyeket a 9.4. alfejezetben írtunk le.

Tudjuk, hogy a rezolúció ismételt alkalmazása megtalálja a bizonyítást, ha létezik. Ebben a részben olyan stratégiákat tekintünk át, amelyek hatékonyan segítenek megtalálni a bizonyításokat.

A tételbizonyítók (amelyeket automatizált következtetőknek is szoktunk nevezni) két szempontból különböznek a logikai programozási nyelvektől. Először is a legtöbb logikai programozási nyelv csak Horn klózokkal dolgozik, ezzel szemben a tételbizonyítások elfogadják a teljes elsőrendű logikát. Másodszor, a Prolog programok egymásba fűzik a logikát és a kontrollt. Ha a programozó választása az A:-B, C-re esik az A:-C, B helyett, ez a program végrehajtására van hatással. A legtöbb tételbizonyításban a mondatok választott szintaktikai formája nincs hatással a kapott eredményekre. A tételbizonyításoknak is szükségük van az információ kontrolljára, hogy hatékonyan működhessenek, de ezt az információt általában külön tárolják a tudásbázistól, ahelyett, hogy magának a tudásreprezentációnak a részeként jelenne meg. A legtöbb kutatás a tételbizonyítások tárgyában magában foglalja az általában hasznos kontrollstratégiákat, amelyek a sebességet is növelhetik.