mgu(s, t)
nach Fallunterscheidung
- s
ist Variable: ...
- t
ist Variable: symmetrisch
-
s = f (s1, s2)
und
t = g(t1, t2)
: ...
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
Johannes Waldmann
2015-12-11