A Unification Algorithm for Associative-Commutative Functions

Publisher Website
Google Scholar
Abstract
An important component of automated theorem-proving systems are unification algorithms which fred most general substitutions which, when apphed to two expressions, make them equivalent Functions which are associative and commutative (such as the arithmetic addition and multiphcatton functions) are often the subject of automated theorem proving An algorithm which unifies terms whose function is associative and commutauve is presented here Termmaaon, soundness, and completeness of the algorithm have been proved for a subclass of the general case. The algorithm is an efficient alternative to other methods of handling associative-commutative functions