Példa Legyen két elsőrendű klóz a

Equation 7.. 

és

pontosan egy komplemens literálpárt tartalmaz. Ha a magjaikat az alapklózokhoz hasonlóan rezolválnánk, a

Equation 7.. 

klózhoz jutnánk. Lássuk be, hogy

Equation 7.. 

Ha

kielégíti a

és

klózokat, a

és

formulák

-ben minden értékelés mellett igazak. Tehát ha egy értékelés mellett

-ben

hamis, akkor ott

igaz, és ha

hamis, akkor

igaz. Mivel minden értékelés mellett

igazsága esetén

hamis és fordítva, így minden értékelés mellett vagy a

, vagy az

igaz, és így

.

Ha ilyen módon képezve elsőrendű klózok rezolvensét szeretnénk ezt rezolúciós levezetési szabályként alkalmazni, akkor igazolni kell általánosan is a példabeli állítást.

Tétel Legyenek most

és

olyan elsőrendű klózok, melyek pontosan egy komplemens literálpárt tartalmaznak, azaz

és

magjai

Equation 7.. 

alakúak, ahol

és

a komplemens literálpár. Legyen a

klóz magja

. Ekkor

.

Bizonyítás Tegyük fel, hogy az

interpretáció kielégíti a

elsőrendű klózhalmazt. Kövessük az előző gondolatmenetet. Az

interpretációban tetszőleges értékelés mellett vagy

és

, vagy

és

igaz. Azaz

-ben

igaz.

Észrevehetjük, hogy komplemens párt ugyan nem tartalmazó két elsőrendű klóz Herbrand-univerzum feletti alappéldányaiban mégis lehet komplemens pár.

Példa

Equation 7.. 

Egyik klózpárban sincs komplemens literálpár. Alaprezolúcióval vizsgáljuk meg, hogy a klózhalmaz kielégíthetetlen-e. A Herbrand-univerzum:

Equation 7.. 

Egy alaprezolúciós levezetés:

Table 7.9. 

		[ ]
		[ , ]
		[ , ]

Tegyünk egy új változót a kiválasztott alapklózokban az

helyébe.

Table 7.10. 

		[ ]
		[ ]
		[ ]

Ez a levezetés a

Equation 7.. 

klózhalmazból való egy elsőrendű rezolúciós levezetés. Ezt a klózhalmazt úgy kaptuk az eredetiből, hogy az elsőrendű klózok magjaiban az atomi formulákban a változók helyébe olyan termeket helyettesítettünk, amelyek azonos alapú literálokat eredményeztek. Ezzel a – logikában egyébként nem megengedett – helyettesítéssel (illesztő helyettesítés)

Tétel Legyen

a

elsőrendű klóz magja. Tegyük fel, hogy

Equation 7.. 

Legyen

tetszőleges termhelyettesítés

leíró nyelvében, és

Equation 7.. 

Ekkor tetszőleges olyan

Herbrand-interpretációban, amelyben

igaz, a

klóz is igaz.

Bizonyítás Tegyük fel, hogy a

Herbrand-interpretációban a

klóz, azaz

igaz. Ekkor

a Herbrand-interpretációbeli minden értékelés mellett igaz, azaz

Herbrand-univerzum feletti alapklózai

-ban igazak. Nyilván

-nak a

feletti alappéldányai mind

feletti alappéldányai is, hisz a

termek jelennek meg az

változók helyett

-ben. Ezek a termek viszont, ha a változóik helyére Herbrand-univerzumbeli elemeket helyettesítünk, szintén Herbrand-univerzumbeli elemek lesznek, és így

alappéldányaiban is előfordulnak.

Definíció Legyen

egy

elsőrendű klózban előforduló legalább két azonos alapú egyformán negált literál alapjainak halmaza. Ha

atomjai illeszthetők egymáshoz és

a

legáltalánosabb illesztő helyettesítése, akkor a

magú klózt a

klóz faktorának nevezzük. Ha a faktor egységklóz, akkor

egységfaktorának hívjuk.

Példa Legyen

. A két

-vel kezdődő atom legáltalánosabb illesztő helyettesítése a

Equation 7.. 

Ennek megfelelően a

Equation 7.. 

klóz a

klóz faktora.

Definíció Legyenek

és

változóikban tiszta klózok. Legyenek

és

magjai rendre

és

alakúak, ahol

és

ellentétesen negált literálok. Ha az

és az

literálok alapjai illeszthetők egymáshoz, legyen

a legáltalánosabb illesztő helyettesítésük. Ekkor a

és

klózok bináris rezolvense a

magú klóz.

Definíció A

és a

klózok elsőrendű rezolvense a következő bináris rezolvensek valamelyike:

Példa Legyen

Equation 7.. 

Mivel

mind

-ben, mind

-ben előfordul, a

-ben átnevezzük. Ezután

. A rezolváláshoz válasszuk az

Equation 7.. 

literálokat. Alapjaik legáltalánosabb illesztő helyettesítése:

. Így tehát a

és a

klózok bináris rezolvense

Equation 7.. 

ahol a

és a

literálok szerint rezolváltunk.

Példa Legyen

Equation 7.. 

A

faktorának magja

.

faktorának és

-nek bináris rezolvense a

klóz. Ennélfogva a

és a

klózok egyik elsőrendű rezolvense

. Tétel Legyen

a

és

elsőrendű klózok elsőrendű rezolvense. Ekkor

.

Bizonyítás

és

változóikban tiszta klózok. Jelöljük

és

elsőrendű rezolvensét – utalva a rezolvensképzés módjára – a következőképpen:

Equation 7.. 

Egy korábban bizonyított tétel miatt, ha az

Herbrand-interpretáció kielégíti

-t, akkor

kielégíti a

klózhalmazt is. Az a két literál, amely szerint rezolváltunk, a

és

klózokban komplemens literálpár, így

Equation 7.. 

Ez viszont azt jelenti, hogy

.

Definíció Egy

klózhalmazból való elsőrendű rezolúciós levezetés elsőrendű klózok egy olyan véges

sorozata, ahol minden

-re

Tétel [Elsőrendű rezolúciós kalkulus helyessége.] Ha egy

klózhalmazból van az üres klóznak elsőrendű rezolúciós levezetése, akkor

kielégíthetetlen.

Bizonyítás Tegyük fel, hogy van az üres klóznak elsőrendű rezolúciós levezetése

-ból:

. Tegyük fel ugyanakkor, hogy van olyan

interpretáció, mely kielégíti a

klózhalmazt. Ezért ha a rezolúciós levezetésben

,

kielégíti

-t. Ha pedig a rezolúciós levezetésben

a

és

klózok elsőrendű rezolvense

és

kielégíti a

és

klózokat, akkor

kielégíti a

rezolvensüket is. Ezért indukcióval könnyen látható, hogy

-nek ki kellene elégítenie a

klózhalmazt is. De

, az üres klóz pedig kielégíthetetlen, tehát

-nak is kielégíthetetlennek kell lennie.

Példa A

Equation 7.. 

klózhalmazból szerkesszünk meg egy elsőrendű rezolúciós levezetést:

Table 7.11. 

		[ ]
		[ faktorizáció, ]

A faktorizáció az elsőrendű rezolúciós elv lényeges eleme, alkalmazása nélkül az elsőrendű rezolúciós eljárás nem lenne teljes.

Példa Adott a következő formulahalmaz:

Equation 7.. 

A formulák alapján kapott klózhalmaz:

Equation 7.. 

Tétel [Elsőrendű rezolúciós kalkulus teljessége.] Ha egy

elsőrendű klózhalmaz kielégíthetetlen, akkor

-ból van az üres klóznak rezolúciós levezetése.