Unifikation--Definition

Unifikationsproblem

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

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

Satz: jedes Unifikationsproblem ist

• entweder gar nicht
• oder bis auf Umbenennung eindeutig

lösbar.