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.

Bsp: Signatur {f /2, a/0} mathend000#,

unifiziere f (X₁, f (X₂, f (X₃, f (X₄, a)))) mathend000# mit f (f (X₂, X₂), f (f (X₃, X₃), f (f (X₄, X₄), f (a, a)))) mathend000#