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/2
R. W. Wilkerson and B. M. McMillin, "Expectations for Associative-Commutative Unification Speedups in a Multicomputer Environment," Proceedings of the 13th Annual International Computer Software and Applications Conference, 1989. COMPSAC 89, Institute of Electrical and Electronics Engineers (IEEE), Jan 1989.
The definitive version is available at https://doi.org/10.1109/CMPSAC.1989.65077
13th Annual International Computer Software and Applications Conference, 1989. COMPSAC 89
Keywords and Phrases
Intel IPSC/2; Abstract Data Types; Associative-Commutative Unification Speedups; Automated Deduction Systems; Commutative Equality Axioms; Formal Logic; General Substitutions; Hybrid AC Unification Algorithm; Inference Mechanisms; Logic Programming; Multicomputer Environment; Parallel; Parallel Algorithms; Parallel Machines; Program Verification; Standard Unification; Symbol Manipulation; Term Rewriting Systems; Termination; Unreasonably Large Search Spaces
Article - Conference proceedings
© 1989 Institute of Electrical and Electronics Engineers (IEEE), All rights reserved.
01 Jan 1989