Unifikation--Komplexität

Bemerkungen:

• gegebene Implementierung ist 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.