Unifikation--Definition

Unifikationsproblem

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

allgemeinst = mathend000# minimal bzgl. der Prä-Ordnung

σ₁≤σ₂$\iff$∃τ : σ₁oτ = σ₂ mathend000#

Satz: jedes Unifikationsproblem ist entweder gar nicht oder bis auf Umbenennung eindeutig lösbar