A Generalized Approach to Equational Unification.
Abstract
Given a set of equational axioms and two terms containing function symbols and variables, the equational unification problem is to find a uniform replacement of terms for the variables that makes the terms provably equal from the axioms. In the general case, the two terms may contain symbols not appearing in the axioms, there may be more than one instance of a set of axioms, and there may be more than one set of axioms. This thesis presents a method for combining equational algorithms to handle the terms with mixed sets of function symbols. For example, given one algorithm for unifying associative-cummutative operators, and another for unifying commutative operators, the author's algorithm provides a method for unifying terms containing both kinds of operators. It is based on a general strategy for decomposing terms and combining unifiers. Attention is restricted to set of axioms whose function symbols are pairwise disjoint.
Document Details
- Document Type
- Technical Report
- Publication Date
- Aug 01, 1985
- Accession Number
- ADA163112
Entities
People
- Katherine A. Yelick
Organizations
- Massachusetts Institute of Technology