Associative-commutative unification (Q1099648)

Unification in equational theories, that is, solving equations in varieties, is of special relevance to automated deduction. Major results in term rewriting systems, as by \textit{G. E. Peterson} and \textit{M. E. Stickel} [J. Assoc. Comput. Mach. 28, 233-264 (1981; Zbl 0479.68092)], depend on unification in presence of associative-commutative functions. \textit{M. E. Stickel} [ibid. 28, 423-434 (1981; Zbl 0462.68075)] 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.