Deciding the Word Problem in the Union of Equational Theories Sharing Constructors
The main contribution of this paper is a new method for combining decision procedures for the word problem in equational the- ories sharing “constructors.” The notion of constructors adopted in this paper has a nice algebraic definition and is more general than a related notion introduced in previous work on the combination problem.
KeywordsNormal Form Word Problem Decision Procedure Equational Theory Free Algebra
Unable to display preview. Download preview PDF.
- 1.F. Baader and K.U. Schulz. Unification in the union of disjoint equational theories: Combining decision procedures. J. Symbolic Computation 21, 1996.Google Scholar
- 2.F. Baader and C. Tinelli. A new approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method. In Proc. CADE-14, Springer LNAI 1249, 1997.Google Scholar
- 3.F. Baader and C. Tinelli. Deciding the word problem in the union of equational theories. UIUCDCS-Report 98-2073, Department of Computer Science, University of Illinois at Urbana-Champaign, 1998. Available at http://www-lti.informatik.rwth-aachen.de/Forschung/Papers.html.
- 4.A. Boudet. Combining unification algorithms. J. Symbolic Computation 16, 1993.Google Scholar
- 5.N. Dershowitz and Z. Manna. Proving termination with multiset orderings. Communications of the ACM 22, 1979.Google Scholar
- 6.E. Domenjoud, F. Klay, and C. Ringeissen. Combination techniques for non-disjoint equational theories. In Proc. CADE-12, Springer LNAI 814, 1994.Google Scholar
- 7.H. Kirchner and Ch. Ringeissen. Combining symbolic constraint solvers on algebraic domains. J. Symbolic Computation 18, 1994.Google Scholar
- 8.T. Nipkow. Combining matching algorithms: The regular case. In Proc. RTA’89, Springer LNCS 335, 1989.Google Scholar
- 9.E. Ohlebusch. Modular properties of composable term rewriting systems. J. Symbolic Computation 20, 1995.Google Scholar
- 10.D. Pigozzi. The join of equational theories. Colloquium Mathematicum 30, 1974.Google Scholar
- 11.Ch. Ringeissen. Unification in a combination of equational theories with shared constants and its application to primal algebras. In Proc. LPAR’92, Springer LNAI 624, 1992.Google Scholar
- 12.Ch. Ringeissen. Combination of matching algorithms. In Proc. STACS-11, Springer LNCS 775, 1994.Google Scholar
- 13.M. Schmidt-Schauff. Combination of unification algorithms. J. Symbolic Computation 8, 1989.Google Scholar
- 15.C. Tinelli and Ch. Ringeissen. Non-disjoint unions of theories and combinations of satisàbility procedures: First results. Technical Report UIUCDCS-R-98-2044, Department of Computer Science, University of Illinois at Urbana-Champaign, April 1998. (Also available as INRIA research report no. RR-3402.)Google Scholar