Definíció Legyen

elsőrendű klózhalmaz, továbbá a

-ban szereplő függvényszimbólumok halmaza

, konstansszimbólumok halmaza

. A

klózhalmaz Herbrand-univerzumán az alábbiakban definiált

halmazt értjük:

Herbrand-bázisa a

-beli termekből épített zárt atomok halmaza.

Példa Legyen

. Mivel

-ban nincs konstansszimbólum, ezért legyen

egy tetszőleges szimbólum.

.

-ban függvényszimbólum sincs, ezért

Equation 7.. 

A klózhalmaz Herbrand-bázisa pedig

Equation 7.. 

Példa Legyen

. Ekkor

Table 7.1. 

	...
		.

Herbrand-bázisa

Equation 7.. 

Példa Legyen

. Ekkor

Table 7.2. 

Definíció Egy

klózhalmaz

leíró nyelve Herbrand-interpretációinak nevezzük és

-vel jelöljük a nyelv olyan interpretációit, melyek univerzuma éppen

,

Egy

elsőrendű klózhalmaz Herbrand-interpretációi tehát csak a

-ban előforduló predikátumszimbólumok interpretálásában különböznek. Ezért világos, hogy

egy

Herbrand-interpretációját a következő módon is leírhatjuk: legyen

Herbrand-bázisa és legyen

Equation 7.. 

Ekkor a

Herbrand-interpretációt az

literál-halmaz egyértelműen megadja.

Példa A

klózhalmaz Herbrand-univerzuma:

Equation 7.. 

Herbrand-bázisa:

Equation 7.. 

Néhány Herbrand-interpretáció:

Table 7.3. 

	=
	=
	=

Az alábbi ábrán bejelöltük az

Herbrand-interpretációkat.

Definíció A

klózhalmaz

leíró nyelvének legyen

valamely

univerzum feletti interpretációja. Az

-nek megfelelő Herbrand-interpretáció

-nak egy olyan

Herbrand-interpretációja, amelyre teljesül, hogy van olyan

Equation 7.. 

függvény, hogy a

zárt atom pontosan akkor igaz

-ban, amikor a (,,neki megfelelő'')

atom az

Equation 7.. 

értékelés mellett igaz

-ben .

Könnyen belátható, hogy egy elsőrendű klózhalmaz nyelvének tetszőleges interpretációjához van megfelelő Herbrand-interpretáció.

Legyen

. Legyen a

a következőképpen definiálva:

Példa Legyen

. Legyen

a következő:

, az

interpretációja

, a predikátum- és függvényszimbólumokhoz pedig az alábbi reláció- és művelettáblákkal definiált relációkat és műveleteket rendeli

.

Table 7.4. 

Table 7.5. 

Table 7.6. 

Herbrand-univerzuma:

Equation 7.. 

Herbrand-bázisa:

Equation 7.. 

Ekkor a

megfeleltetés:

Equation 7.. 

Az

-nek megfelelő Herbrand-interpretáció:

Equation 7.. 

Példa Legyen

. Vegyük észre, hogy

leíró nyelve az előző példabeli leíró nyelvtől csak abban különbözik, hogy ebben nincs konstansszimbólum. Interpretáljuk

nyelvét az

interpretációval, ami csak annyiban különbözik

-től, hogy konstansszimbólumot nyilván nem kell interpretálnia. Most a

megfeleltetés során

-hoz bármely univerzumelem hozzárendelhető. Tartsuk meg a többi Herbrand-univerzumbeli elemre az előző példabeli megfeleltetést.

Tétel Ha egy

interpretáció kielégít egy

elsőrendű klózhalmazt, akkor az

-nek megfelelő Herbrand-interpretáció is kielégíti

-t.

Bizonyítás A definíció szerint ha

az

-nek megfelelő Herbrand-interpretáció, akkor van olyan

függvény, hogy minden

esetén az

a

-hez ugyanazt az igazságértéket rendeli, mint az

a

atomhoz az

Equation 7.. 

értékelés mellett.

Tétel Egy

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

-t nem elégíti ki a Herbrand-univerzuma feletti egyetlen Herbrand-interpretáció sem.

Bizonyítás

Egyik tétel sem áll fenn, ha

nem elsőrendű klózhalmaz. Vagyis, ha

zárt formulák tetszőleges halmaza, akkor általában nem igaz, hogy

kielégíthetetlenségének vizsgálata esetén elég lenne

-át csak a Herbrand-struktúrákkal interpretálni.

Példa Legyen

. A

kvantoros formulája nem elsőrendű klóz.

Herbrand-univerzuma:

,

Herbrand-bázisa:

. A

formulahalmazt egyik Herbrand-interpretáció sem elégíti ki. Azonban

kielégíthető, hiszen az az

feletti

interpretáció, melyben

,

és

, kielégíti

-át.

Definíció Legyen

egy klóz,

pedig

Herbrand-univerzuma. Legyen a

Equation 7.. 

termhelyettesitésben

. Ez a helyettesítés

egy, a Herbrand-univerzum feletti értékelése. A

formulát a

klóz egy

feletti alappéldányának nevezzük.

Példa A

klózhalmaz klózainak Herbrand-univerzum feletti alappéldányai:

Equation 7.. 

Tétel [Herbrand tétele] Egy

elsőrendű klózhalmaz akkor és csak akkor kielégíthetetlen, ha a

klózai Herbrand-univerzum feletti alappéldányainak van véges, itt kielégíthetetlen részhalmaza.

Példa