Unifikation--Definition

Unifikationsproblem

• Eingabe: Terme t₁, t₂∈Term(Σ, V)
• Ausgabe: eine allgemeinster Unifikator (mgu): Substitution σ mit t₁σ = t₂σ.

(allgemeinst: minimal bzgl. $\raisebox{-8pt}[0pt][0pt]{$\stackrel{\displaystyle <}{\sim}$}$)

Satz: jedes Unifikationsproblem ist

• entweder gar nicht
• oder bis auf Umbenennung eindeutig

lösbar.