Unifikationsproblem (unvollst.)
- Eingabe: Terme
t1, t2∈Term(Σ, V)
- Ausgabe: eine Substitution
σ = mgu(t1, t2)
mit:
- σ
unifiziert t1, t2
:
t1σ = t2σ
.
Beispiele: bestimme jeweils Menge der Unifikatoren von:
-
f (X), f (a)
- X, f (Y)
-
f (X), g(Y)
- X, f (X)
Für den Fall mehrerer Unifikatoren
möchte man bestimmte auswählen.
(
⇒
vollst. Def. nächste Folie)
Johannes Waldmann
2015-12-11