ISSN:
1573-0670
Keywords:
Unification
;
associativity
;
commutativity
;
Abelian monoids
;
Abelian semigroups
;
automated theorem proving
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
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 unifiction of terms in the presence of an associative and commutative function, 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 unfiers is closely related to the notion of a basis for the linear solution space of these equations. This result is extended to unification in free term algebras combined with Abelian semigroups.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF00243791
Permalink
