7.4. Rezolúciós levezetési stratégiák

7.4.1. 1. A teljes szintek módszere

Legyen

tetszőleges klózhalmaz. A teljes szintek módszere a következőképpen állítja elő a levezetéshez a rezolvenseket:

  1. ,

    .

  2. Ha

    , sikeresen vége. Egyébként

    és folytassuk a 2. lépéssel.

Ezzel a módszerrel sok egyforma klóz jelenik meg a rezolvensek között, sőt olyan rezolvens klózok is a klózhalmazba kerülhetnek, amelyekre a továbblépésben biztosan nincs szükség. E problémák megoldására született meg a törlési stratégia.

7.4.2. 2. A törlési stratégia

Minden

esetén az

klózhalmazból el kell hagyni a fölösleges klózokat: a tautológiákat és azokat, amelyeket más klózok ,,tartalmaznak''.

Definíció Jelölje

és

rendre a

és a

klózok literáljainak halmazát. Egy

klóz befoglalja a

klózt, ha van olyan

termhelyettesítés, hogy

.

a befoglalt klóz.

Példa Legyen

és

. Ekkor

és

. Ha

, akkor

.

, tehát

befoglalja

-t.

A tautológiákat és a befoglalt klózokat meg kell találni. A tautológiákat a faktorizáció segítségével fedhetjük fel. A befoglalási teszt azonban nem olyan egyszerű.

7.4.2.1. Befoglalási algoritmus

Legyenek

és

klózok. Legyen

, ahol

a

-ben előforduló változók és

sem

-ben, sem

-ben elő nem forduló különböző konstansszimbólumok. Tegyük fel, hogy

.

  1. ,

    ,

    ,

  2. Ha

    , akkor vége:

    befoglalja

    -t. Egyébként

    Equation 7.. 


  3. Ha

    üres, akkor vége:

    nem foglalja be

    -t. Egyébként

    , és folytatás a 2. lépéssel.

Példa Befoglalja-e

a

-t?

Equation 7.. 


változói az

és a

. Legyen

. Ekkor

Equation 7.. 


  1. ,

    .

  2. Mivel

    , azt kapjuk, hogy

    Equation 7.. 


  3. Mivel

    és az

    , az eljárást folytatva kapjuk, hogy

    .

  4. Mivel

    , az eljárásnak vége:

    befoglalja

    -t.