Unifikation--Definition (vollst.)

• Eingabe: Terme t₁, t₂∈Term(Σ, V)
• Ausgabe: eine Substitution σ = mgu(t₁, t₂) mit:
  • σ unifiziert t₁, t₂ : t₁σ = t₂σ .
  • σ ist minimal bzgl. ≤ unter allen Unifikatoren von t₁, t₂

benutzt Prä-Ordnung auf Substitutionen:

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

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

Bem: Prä-Ordung: transitiv und symmetrisch. (Beweis?)

Warum ist ≤ keine Halbordnung?