Unifikation--Begriffe

• Substitution: partielle Abbildung σ : V→Term(Σ, V) ,

  so daß kein v∈domσ in imgσ vorkommt.

• Substitution σ auf Term t anwenden: tσ

  (definiert durch Induktion über t )

• Produkt von Substitutionen: so definiert, daß t(σ₁oσ₂) = (tσ₁)σ₂

  (wie geht das genau?)

• die so definierten Substitutionen sind idempotent: σoσ = σ .