Unifikation--Definition

Unifikationsproblem

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

(allgemeinst: minimal bzgl. )

Satz: jedes Unifikationsproblem ist

• entweder gar nicht
• oder bis auf Umbenennung eindeutig

lösbar.

(σ ist Umbenennung: imgσ⊆ Variablen)