Chapter 7. A rezolúciós kalkulus

7.1. A Herbrand-univerzum és az elsőrendű klózhalmazok

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:

  1. Legyen

  2. Legyenek továbbá, ha

    rendre

    , ahol

    .

  3. Végül legyen

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

,

  • minden

    konstansszimbólumhoz

    a

    univerzumelemet (önmagát) rendeli, és

  • minden

    aritású

    függvényszimbólumhoz

    hozzárendeli azt az

    műveletet, amelyikre minden

    esetén

    Equation 7.. 


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:

  • ha

    , akkor a

    -ban szereplő extra konstanshoz

    rendeljen tetszőleges

    -beli elemet,

  • minden

    (egyúttal

    ) konstansszimbólum esetén

    legyen az

    -beli elem,

  • az

    alakú

    -beli elemek esetén

    legyen a

    -beli elem.

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.

  • Ha

    , akkor az

    -nek megfelelő Herbrand-interpretáció a fenti

    .

  • Ha

    , az

    -nek megfelelő Herbrand-interpretáció

    Equation 7.. 


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

  1. Tegyük fel, hogy

    kielégíthetetlen. Ekkor

    -t nem elégítheti ki (semmilyen univerzum felett) egyetlen interpretáció sem, így egyetlen Herbrand-interpretáció sem.

  2. Tegyük fel, hogy

    ugyan kielégíthetetlen az általa meghatározott Herbrand-univerzumon, de

    nem kielégíthetetlen, azaz van olyan

    univerzum és

    interpretáció, amely

    -t kielégíti. Legyen

    a

    -nek megfelelő Herbrand-interpretáció. Az előző tétel miatt

    kielégíti

    -t, pedig

    a Herbrand-univerzum feletti interpretáció. Ellentmondásra jutottunk, tehát ha

    kielégíthetetlen a Herbrand-univerzumán, akkor

    kielégíthetetlen.

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

  1. Legyen

    . Az

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

    Herbrand-univerzum feletti alappéldányainak

    Equation 7.. 


    egy véges kielégíthetetlen részhalmaza.

  2. A

    kielégíthetetlen, mert

    Herbrand-univerzum feletti alappéldányainak

    Equation 7.. 


    egy véges, kielégíthetetlen részhalmaza. Ezek az alappéldányok az

    Equation 7.. 


    értékelés mellett álltak elő.