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 (Ü)
• mit komprimierter Darstellung: Linearzeit.

autotool-Quelltexte Substitution und Unifikation: http://autolat.imn.htwk-leipzig.de/gitweb/?p=tool;a=tree;f=collection/src/Prolog;hb=for-ghc-7.8