Unifikation--Algorithmus

mgu(s, t) nach Fallunterscheidung

• s ist Variable: ...
• t ist Variable: symmetrisch
• s = f (s₁, s₂) und t = g(t₁, t₂): ...

Bemerkungen:

• korrekt, übersichtlich, aber nicht effizient,
• es gibt Unif.-Probl. mit exponentiell großer Lösung,
• eine komprimierte Darstellung davon kann man aber in Polynomialzeit ausrechnen.