Abstract
Unification algorithms are an essential component of automated reasoning and term rewriting systems. Unification finds a set of substitutions or unifiers that, when applied to variables in two or more terms, make those terms identical or equivalent. Most systems use Robinson's unification algorithm or some variant of it. However, terms containing functions exhibiting properties such as associativity and commutativity may be made equivalent without appearing identical. Systems employing Robinson's unification algorithm must use some mechanism separate from the unification algorithm to reason with such functions. Often this is done by incorporating the properties into a rule base and generating equivalent terms which can be unified by Robinson's algorithm. However, rewriting the terms in this manner can generate large numbers of useless terms in the problem space of the system.
If the properties of the functions are incorporated into the unification algorithm itself, there is no need to rewrite the terms such that they appear identical. Stickel developed an algorithm to unify two terms containing associative and commutative functions. The unifiers (there may be more than one) are found by creating a homogeneous linear Diophantine equation with integer coefficients from the terms being unified. The unifiers can be constructed from solutions to this equation.
The unifiers generated from one solution of the Diophantine equation are independent of any other solution to the equation. Therefore, once the Diophantine equation has been solved, the unifiers can be calculated from the solutions in parallel. We have implemented Stickel's AC unification algorithm to run in parallel on a local area network of Sun 4/110 workstations in an effort to improve the speed of AC unification.
Recommended Citation
Kleikamp, David John and Wilkerson, Ralph W., "A Parallel Implementation of Stickel's AC Unification Algorithm in a Message-Passing Environment" (1988). Computer Science Technical Reports. 76.
https://scholarsmine.mst.edu/comsci_techreports/76
Department(s)
Computer Science
Report Number
CSc-88-11
Document Type
Technical Report
Document Version
Final Version
File Type
text
Language(s)
English
Rights
© 1988 University of Missouri--Rolla, All rights reserved.
Publication Date
December 1988
Comments
This report is substantially the M.S. thesis of the first author, completed, December 1988.