Expectations for Associative-Commutative Unification Speedups in a Multicomputer Environment

An essential element of automated deduction systems is unification algorithms which identify general substitutions and when applied to two expressions, make them identical. However, functions which are associative and commutative, such as the usual addition and multiplication functions, often arise in term rewriting systems, program verification, the theory of abstract data types and logic programming. The introduction to the associative and commutative equality axioms together with standard unification brings with it problems of termination and unreasonably large search spaces. One way around these problems is to remove the troublesome axioms from the system and to employ a unification algorithm which unifies modulo the axioms of associativity and commutativity. Unlike standard unification, the associative-commutative (AC) unification of two expressions can lead to the formation of many most general unifiers. A report is presented on a hybrid AC unification algorithm which has been implemented to run in parallel on an Intel iPSC/