Unification in linear time and space: a structured presentation

Unification was introduced by J.A. Robinson in the context of automatic theorem proving and plays an important role in many areas of symbolic manipulation. We present a general framework where all known algorithms for unification can be described, and in this context we introduce the most general version of our algorithm. Two alternative refinements are then exposed, the first leading with the total number of syblos and n log n with the number of distinct variables; the second to a more complicated linear algorithm. Full complexity analysis of both algorithms is included.