Wiederholung: Bestimmung des mgu

• falls s = t, dann return identische Abbildung
• falls s Variable
  • falls s in t vorkommt, dann fail
  • sonst return (s $\mapsto$ t)
• falls t Variable entsprechend
• falls s = f (x₁,…) und t = g(y₁,…), dann
  • falls f≠g, dann fail, sonst ...
  • bestimme σ = mgu(x₁, y₁)
  • return σ∪mgu((x₂σ,…),(y₂σ,…))

Dieser Algorithmus ist korrekt, aber nicht effizient.