7.2. Az alaprezolúció

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ó

  1. vagy olyan, hogy

    igaz benne, de

    hamis (

    ),

  2. vagy olyan, hogy

    igaz benne, de

    hamis (

    ).

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

  1. vagy

    ,

  2. vagy van olyan

    , hogy

    a

    klózpár rezolvense,

é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

  1. A levezetés első klóza,

    , biztosan eleme

    -nak, tehát

    .

  2. Tegyük most fel, hogy minden

    -re igazoltuk már, hogy

    .

  3. Belátjuk, hogy

    -re is igaz az állítás. Ha

    , akkor

    . Ha

    valamely

    klózok rezolvense, akkor az előző tétel miatt

    . Az indukciós feltevés miatt

    és

    . Ebből

    .

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.