Unification in abelian semigroups (Q1098653)

As always when Professor J. Siekmann takes the floor, he has really something to say. His experience and results [Lect. Notes Comput. Sci. 170, 1-42 (1984; Zbl 0547.03011); Automation of reasoning: Classical papers on computational logic. Vol. 1: 1957-1966, Vol. 2: 1967-1970 (1983; Zbl 0567.03001, Zbl 0567.03002)] are strong arguments. The paper is a thorough investigation on associative-commutative (AC- )unification, a theoretical basis, bringing also improvements of the techniques and algorithms at each stage of the general AC-unification problem. We just point out some of the questions raised in the paper. The first section begins with a review of the contributions to the AC- unification problem solving: After first basic results in \textit{M. E. Stickel} [(*)\ J. Assoc. Comput. Mach. 28, 423-434 (1981; Zbl 0462.68075)], and \textit{M. Livesey} and the second author [(**)\ Unification of AC-terms (bags) and ACI-terms (sets), Internal Report, Univ. Essex (1975), and Technical Report 3-76, Univ. Karlsruhe (1976)], further results belong to G. Huet, J. M. Hullot, F. Fages, A. Fortenbacher, C. Kirchner, and others. The key moments in solving the problem were: (1) the (independent) essential observation in (*) and (**) of the relationship between the AC-unification problem and the solving of linear (homgeneous in (*) and inhomogeneous in (**)) diophantine equations, as well as of the fact (deriving from a previously known mathematical result) that the set of the most general unifiers is always finite for the AC-unification procedure; (2) the termination of the extended AC-unification procedure, solved by \textit{F. Fages} [Lect. Notes Comput. Sci. 170, 194-208 (1984; Zbl 0547.03012)] by using an induction argument on a complexity measure on AC-tems. A still open problem remains that of a minimality condition for the extended AC-unification algorithm. Section 2 presents the complete solution of the unification in abelian monoids, following the original ideas in (**). {\S} 2.5 is devoted to a detailed comparison of the authors' solution and that belonging to Stickel (*), emphasizing the advantages of the present approach but also the recent improvements of Stickel's approach. The present algorithm is stated in general terms both for AC-operators with or without unit. Section 3 presents the extension of the AC-unification algorithm to first order terms containing uninterpreted function symbols. The solutions are also different from those of Stickel's algorithm: while this makes a ``variable abstraction'', the authors' reduction is of the ``constant abstraction'' type, the subterms being replaced by ``special'' constants in the reduction process. The classical J. A. Robinson's unification algorithm is combined, after the reduction process, with diophantine equation procedures, ``merging'' the unifiers of the two processes. The correctness and completeness of the extended AC-unification are proved. F. Fages' complexity measure is slightly modified (constants not being alien subterms) to prove, by noetherian induction on this measure, the termination of the algorithm. All the notions and proofs are most clearly exposed and exemplified. The paper is, we think, a serious candidate to the future ``elections'' for an (eventually, but so much desired) forthcoming ``Classical papers on computational logic'' new volume.