Unification in Abelian Semigroups

Abstract

Unification in equational theories, i.e. solving of equations in varieties, is a basic operation in Computational Logic, in Artificial Intelligence (AI) and in many applications of Computer Science. In particular the unification of terms in the presence of an associative and commutative f unction, i.e. solving of equations in Abelian Semigroups, turned out to be of practical relevance for Term Rewriting Systems, Automated Theorem Provers and many AI-programming languages. The observation that unification under associativity and commutativity reduces to the solution of certain linear diophantine equations is the basis for a complete and minimal unification algorithm. The set of most general unifiers is closely related to the notion of a basis for the linear solution space of these equations. These results are extended to unification in free term algebras combined with Abelian Semigroups.