Paper Info
Title
Unification in combinations of collapse-free regular theories
Abstract
This paper presents a method for combining equational unification algorithms to handle terms containing 'mixed' sets of function symbols. For example, given one algorithm for unifying associative-commutative operators, and another for unifying commutative operators, our algorithm provides a method for unifying terms containing both kinds of operators. As a special case of the combining problem, our algorithm lifts a variable-only case algorithm to the general case with multiple operator instances and free symbols. We restrict our attention to a class of equational theories called the collapse-free regular theories. We give some results characterizing the unification problem in this class of theories, and specifically show the restrictions are necessary and sufficient for the correctness of our algorithm. An implementation has been done as part of a larger system for reasoning about equational theories.
Year
DOI
Venue
1987
10.1016/S0747-7171(87)80025-1
J. Symb. Comput.
Keywords
DocType
Volume
special case,unifying associative-commutative operator,equational unification algorithm,unification problem,variable-only case algorithm,unifying commutative operator,equational theory,collapse-free regular theory,unifying term,general case
Journal
3
Issue
ISSN
Citations 
1-2
Journal of Symbolic Computation
26
PageRank 
References 
Authors
3.80
23
1
Name
Order
Citations
PageRank
Katherine A. Yelick13494407.23