Bestimmung des mgu

(vergleiche Logische Programmierung)

• 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 $\neq$ g, dann fail, sonst ...
  • bestimme $\sigma$ = mgu(x₁, y₁)
  • return $\sigma$ $\cup$ mgu((x₂$\sigma$,...),(y₂$\sigma$,...))

Dieser Algorithmus ist korrekt, aber nicht effizient.