A Complete Unification Algorithm for Associative-Commutative Functions
Abstract
An important component of mechanical theorem proving systems are unification algorithms which find most general substitutions which, when applied to two expressions, make them equivalent. Functions which are associative and commutative (such as the arithmetic addition and multiplication functions) are often the subject of mechanical theorem proving. An algorithm which unifies terms whose function is associative and commutative is presented here. The algorithm eliminates the need for axiomatizing the associativity and commutativity properties and returns a complete set of unifiers without recourse to the indefinite generation of variants and instances of the terms unified required by previous solutions to the problem.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 01, 1975
- Accession Number
- ADA015846
Entities
People
- Mark E. Stickel
Organizations
- Carnegie Mellon University