Wiederholung: Unifikation

• ein Unifikator von zwei Termen s, t∈Term(Σ, V)

  ist eine Substitution σ : V→Term(Σ, V) mit tσ = sσ

• zwei Terme s, t können keinen, einen oder mehrere Unifikatoren haben
• Substitutionen nacheinander ausführen: σoτ

• Substitutionen ordnen durch σ₁≤σ₂ (σ₁ ist allgemeiner als σ₂) falls ∃τ : σ₂ = σ₁oτ

• Satz: Wenn s, t unifizierbar, dann gibt es einen allgemeinsten Unifikator (most general unifier) σ von s und t: für jeden Unifikator σ₂ von s und t gilt σ≤σ₂.

  mgu(s, t) ist bis auf Umbennenung eindeutig.