Ha Herbrand tételét szeretnénk felhasználni egy klózhalmaz kielégíthetetlenségének vizsgálatára, a klózhalmaz Herbrand-univerzum feletti alappéldányai halmazában kell keresnünk kielégíthetetlen, véges részhalmazt. Egy elsőrendű klóz alappéldányai zárt literálok elemi diszjunkciói, tehát maguk is klózok. Ebben a szakaszban most csak ilyen klózokkal dolgozunk: zárt atomok és negáltjaik elemi diszjunkcióival. Nevezzük őket alapklózoknak . Egy atomot és negáltját komplemens literálpárnak fogjuk nevezni.

Definíció Legyen a

és

alapklózokban az egyetlen komplemens literálpár

és

. A

klózt a

klózpár rezolvensének , az

és

literálokat pedig a kirezolvált literáloknak nevezzük. Ha

és

, rezolvensük az üres klóz (

).

Példa Vizsgáljunk most meg néhány klózpárt, van-e rezolvensük.

Table 7.7. 

	klózpár	rezolvens
(a)
(b)		nincs komplemens literálpár
(c)		nincs komplemens literálpár
(d)		két komplemens literálpár van
(e)

Tétel Legyenek

és

, ahol

és

az egyetlen komplemens literálpár.

.

Bizonyítás Ha

és

, akkor nincs a

klózhalmazt kielégítő interpretáció, tehát igaz az állítás. Egyébként a

klózhalmazt kielégítő tetszőleges interpretáció

Mivel az

interpretáció kielégíti a

klózhalmazt, azaz itt a

és a

klózok igazak, de

hamis, ezért

igaz, tehát igaz

is. Hasonlóképpen láthatjuk be, hogy az

interpretációkban pedig

igaz. Tehát mind

, mind

kielégíti a

klózt.

Definíció Egy

alapklózhalmazból a

klóz rezolúciós levezetése egy olyan véges

klózsorozat, ahol minden

-re

és klózsorozat utolsó tagja,

, éppen a

klóz.

Példa Próbáljuk meg az üres klózt levezetni a

Equation 7.. 

klózhalmazból. A levezetés bármelyik

-beli klózzal indítható.

Table 7.8. 

		[ ]
		[ ]
		[ 1, 2 rezolvense ]
		[ ]
		[ 2, 4 rezolvense ]
		[ 3, 5 rezolvense ]
		[ ]
		[ 6, 7 rezolvense ]
		[ ]
		[ 8, 9 rezolvense ]
		[ 5, 10 rezolvense ]

Lemma Legyen

tetszőleges alapklózhalmaz és a

klózsorozat rezolúciós levezetés

-ból. Ekkor

minden

-re következménye az

klózhalmaznak, azaz

.

Bizonyítás

Tétel [A rezolúciós kalkulus helyessége.] Legyen

tetszőleges alapklózhalmaz. Ha

-ból levezethető az üres klóz, akkor

kielégíthetetlen.

Bizonyítás Tegyük fel, hogy van olyan

interpretáció, ami kielégíti

-t. Az előbbi lemma szerint egy

-ból való rezolúciós levezetésbeli bármely

klózra

, tehát

kielégíti a rezolúciós levezetés minden klózát is. De az üres klóz kielégíthetetlen, tehát nem lehet eleme a levezetésnek. Így tehát ha

-ból levezethető az üres klóz, akkor

kielégíthetetlen.

Tétel [A rezolúciós kalkulus teljessége.] Ha a

véges alapklózhalmaz kielégíthetetlen, akkor

-ból levezethető az üres klóz.