Unifikation--Algorithmus

mgu(s, t) mathend000# nach Fallunterscheidung

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

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.