3.2. Illesztő helyettesítés

Definíció Legyen

és

két azonos predikátumszimbólummal kezdődő atomi formula. Az olyan

termhelyettesítést, amelyre

Equation 3.. 


-t és

-t egymáshoz illesztő helyettesítésnek nevezzük.

az

és

atomok legáltalánosabb illesztő helyettesítése , ha

és

minden illesztő helyettesítésénél általánosabb.

Példa A

és a

atomoknak egy illesztő helyettesítése:

Equation 3.. 


legáltalánosabb illesztő helyettesítése:

Equation 3.. 


Az illesztő helyettesítés fogalmát kiterjeszthetjük:

legyen az azonos predikátumszimbólummal kezdődő

(

) atomi formulák halmaza.

illesztő helyettesítése

minden atompárját illeszti egymáshoz.

Definíció Vizsgáljuk

elemeit párhuzamosan, szimbólumonként balról jobbra haladva. Álljunk meg annál az első szimbólumnál, amelyik nem minden atomban egyezik meg. Az ezen a pozíción kezdődő résztermek

halmazát

különbségi halmazának nevezzük.

Példa Legyen

Equation 3.. 


különbségi halmaza

Equation 3.. 


Robinson algoritmusa véges sok lépésben meghatározza

legáltalánosabb illesztő helyettesítését, ha van ilyen, illetve jelzi, ha nem illeszthetők egymáshoz

atomjai.

  1. ,

    ,

    .

  2. Ha

    egyetlen atomot tartalmaz, akkor sikeresen vége:

    a

    legáltalánosabb illesztő helyettesítése. Egyébként határozzuk meg

    különbségi halmazát:

    -t.

  3. Ha van

    -ban olyan

    változó és

    term, hogy

    nem fordul elő

    -ban, akkor a 4. lépéssel folytatjuk. Egyébként

    atomjai nem illeszthetők egymáshoz. Vége.

  4. ,

    . (Megjegyezzük, hogy

    .)

  5. , és a 2. lépéssel folytatjuk.

Példa Döntsük el az illesztő algoritmussal, hogy illeszthetők-e a

Equation 3.. 


halmaz atomi formulái egymáshoz.

  1. ,

    .

  2. .

  3. egy változó,

    egy, a

    -t nem tartalmazó term.

  4. .

    Equation 3.. 


  5. egy változó,

    egy, az

    -et nem tartalmazó term.

  6. .

    Equation 3.. 


  7. .

  8. egy változó,

    egy, az

    -t nem tartalmazó term.

  9. .

    Equation 3.. 


  10. -ban egyetlen atom van, így

    a legáltalánosabb illesztő helyettesítés

    -re.

Példa Vizsgáljuk meg, hogy illeszthetők-e egymáshoz a

Equation 3.. 


halmaz atomi formulái.

  1. ,

    .

  2. .

  3. egy változó,

    egy, az

    -t nem tartalmazó term.

  4. .

    Equation 3.. 


  5. .

  6. A

    -ben nincs változó, ezért az algoritmus azzal az eredménnyel fejeződik be, hogy

    atomjai nem illeszthetők.

Az illesztő helyettesítés fogalmát másképp is általánosíthatjuk:

legyen az

Equation 3.. 


páronként azonos predikátumszimbólummal kezdődő atomi formulák halmaza. Keressük a minden pár atomjait egymáshoz illesztő helyettesítést. Képezzük a

-beli párok atomjaiból a

Equation 3.. 


formális egyenlőséghalmazt. A formális egyenlőséghalmazba bizonyos szabályok alapján bekerülhetnek termek formális egyenlőségei, illetve ki is kerülhetnek a halmazból formális egyenlőségek. Egy csupa változó - term párokból álló

Equation 3.. 


formális egyenlőséghalmaz kiszámított alakú , ha

, amikor

, és

(

). Az előbbi kiszámított alakú formális egyenlőséghalmaz által meghatározott termhelyettesítés

Equation 3.. 


Herbrand algoritmusa véges sok lépésben meghatározza

legáltalánosabb illesztő helyettesítését, ha van ilyen, illetve jelzi, ha nem illeszthetők egymáshoz

párjainak atomjai.

  1. ,

    .

  2. Ha

    kiszámított alakú, akkor sikeresen vége: az általa meghatározott helyettesítés

    legáltalánosabb illesztő helyettesítése. Egyébként válasszunk ki egy

    formális egyenlőséget

    -ból.

  3. .

  4. Ha

    alakja

    • , ahol

      változó, vagy

      , ahol

      konstansszimbólum, akkor tovább az 5. lépésre.

    • , ahol

      változó,

      összetett term,

      .

    • , ahol

      konstansszimbólumok, akkor

      atomjai nem illesztők egymáshoz. Vége.

    • , ahol

      függvényszimbólumok, akkor

      atomjai nem illesztők egymáshoz. Vége.

    • , ahol

      függvényszimbólum, vagy

      , ahol

      predikátumszimbólum, akkor

      .

    • , ahol

      , akkor

      atomjai nem illesztők egymáshoz. Vége.

    • , ahol

      , akkor

      formális egyenlőségeiben elvégezzük az

      helyettesítést, majd

      .

  5. , és a 2. lépéssel folytatjuk.

Példa Döntsük el Herbrand algoritmusával, hogy illeszthetők-e a

Equation 3.. 


halmaz atomi formulái egymáshoz.

Equation 3.. 


Kiszámított alakú formális egyenlőséghalmazt kaptunk, így a legáltalánosabb illesztő helyettesítés

-re:

.

Példa Döntsük el Herbrand algoritmusával, hogy illeszthetők-e a

Equation 3.. 


halmaz atomi formulái egymáshoz.

Equation 3..