Unification in commutative idempotent monoids (Q1111775)

The paper is related to the algebraic theory of abstract data types and deals with the unification of the algorithms as to associativity, commutativity, and idempotence of the function unions from which the discussed algorithms are constructed. The investigation goes back to the unification in commutative semigroups (AC-unification) and in commutative idempotent semigroups (ACI-unification) [\textit{M. Liversey} and \textit{J. Siekmann}, Unification of sets and multisets, Tech. Rep., University of Karlsruhe, 1976]. ACI-unification is associated with the congruence relation on the totality of free terms. The problems of ACI-unification for free idempotent commutative monoids have been discussed by the second author [Lect. Notes Comput. Sci. 230, 470-488 (1986; Zbl 0643.68136)]. The main result of this paper is the construction of a minimal complete set of unifiers for idempotent commutative monoids. The ACI-unification correctness is established. In spite of finiteness of the complete set of unifiers, the power of the set is rather high and this determines mainly the theoretical value of the obtained results. The investigation is of interest for applications to automatic theorem proving, term-rewrite systems, logic and functional programming.