Definíció Legyen
és
két azonos predikátumszimbólummal kezdődő atomi formula. Az olyan
termhelyettesítést, amelyre
-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:
legáltalánosabb illesztő helyettesítése:
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
különbségi halmaza
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.
,
,
.
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.
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.
,
. (Megjegyezzük, hogy
.)
, és a 2. lépéssel folytatjuk.
Példa Döntsük el az illesztő algoritmussal, hogy illeszthetők-e a
halmaz atomi formulái egymáshoz.
,
.
.
egy változó,
egy, a
-t nem tartalmazó term.
.
egy változó,
egy, az
-et nem tartalmazó term.
.
.
egy változó,
egy, az
-t nem tartalmazó term.
.
-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
halmaz atomi formulái.
,
.
.
egy változó,
egy, az
-t nem tartalmazó term.
.
.
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
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
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ó
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
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.
,
.
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.
.
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
.
, és a 2. lépéssel folytatjuk.
Példa Döntsük el Herbrand algoritmusával, hogy illeszthetők-e a
halmaz atomi formulái egymáshoz.
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
halmaz atomi formulái egymáshoz.
