Associative-commutative unification

Unification in equational theories, that is, solving equations in varieties, is of special relevance to automated deduction. Major results in term rewriting systems, as in (Peterson & Stickel, 1981; Hsiang, 1982), depend on unification in presence of associative-commutative functions. (Stickel, 1975; Stickel, 1981) gave an associative-commutative unification algorithm, but its termination in the general case was still questioned. The first part of this paper is an introduction to unification theory, the second part concerns the solving of homogeneous linear diophantine equations, and the third contains a proof of termination and correctness of the associative-commutative unification algorithm for the general case.