7.3. Az elsőrendű rezolúció

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:

  1. a

    és a

    klózok bináris rezolvense,

  2. a

    klóz és a

    klóz egy faktorának a bináris rezolvense,

  3. a

    klóz egy faktorának és a

    klóznak a bináris rezolvense,

  4. a

    klóz egy faktorának és a

    klóz egy faktorának a bináris rezolvense.

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

  1. vagy

    ,

  2. vagy van olyan

    , hogy

    a

    és

    klózok elsőrendű rezolvense.

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.. 


  1. A Herbrand-univerzum:

    . A Herbrand-bázis:

    . A

    feletti alapklózhalmaz:

    . Alaprezolúciós levezetés:

    Table 7.12. 

    [ 1, 2 rezolvense ]

    [ 1, 4 rezolvense ]

    [ 3, 5 rezolvense ]

  2. Elsőrendű rezolúciós levezetés

    -ból, faktorizáció nélkül:

    Table 7.13. 

    [ 1, 2 rezolvense ]

    [ 1, 4 rezolvense ]

    A levezetés nem folytatható, mivel nincs olyan klózpár, amely egyetlen komplemens literálpárt tartalmazna. Így az üres klózt nem kapjuk meg.

  3. Rezolúciós levezetés

    -ból, faktorizációval:

    1. Alkalmazzuk

      klózaira a

      legáltalánosabb illesztő helyettesítést.

      Equation 7.. 


    2. A levezetés

      -ból:

      Table 7.14. 

      [ 1, 2 rezolvense ]

      [ 1, 4 rezolvense ]

      [ 3, 5 rezolvense ]

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.