Abstract
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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
F. Baader and K.U. Schulz. Unification in the union of disjoint equational theories: Combining decision procedures. J. Symbolic Computation 21, 1996.
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.
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.
A. Boudet. Combining unification algorithms. J. Symbolic Computation 16, 1993.
N. Dershowitz and Z. Manna. Proving termination with multiset orderings. Communications of the ACM 22, 1979.
E. Domenjoud, F. Klay, and C. Ringeissen. Combination techniques for non-disjoint equational theories. In Proc. CADE-12, Springer LNAI 814, 1994.
H. Kirchner and Ch. Ringeissen. Combining symbolic constraint solvers on algebraic domains. J. Symbolic Computation 18, 1994.
T. Nipkow. Combining matching algorithms: The regular case. In Proc. RTA’89, Springer LNCS 335, 1989.
E. Ohlebusch. Modular properties of composable term rewriting systems. J. Symbolic Computation 20, 1995.
D. Pigozzi. The join of equational theories. Colloquium Mathematicum 30, 1974.
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.
Ch. Ringeissen. Combination of matching algorithms. In Proc. STACS-11, Springer LNCS 775, 1994.
M. Schmidt-Schauff. Combination of unification algorithms. J. Symbolic Computation 8, 1989.
E. Tidén. First-Order Unification in Combinations of Equational Theories. Phd thesis, The Royal Institute of Technology, Stockholm, 1986.
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.)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baader, F., Tinelli, C. (1999). Deciding the Word Problem in the Union of Equational Theories Sharing Constructors. In: Narendran, P., Rusinowitch, M. (eds) Rewriting Techniques and Applications. RTA 1999. Lecture Notes in Computer Science, vol 1631. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48685-2_14
Download citation
DOI: https://doi.org/10.1007/3-540-48685-2_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66201-3
Online ISBN: 978-3-540-48685-5
eBook Packages: Springer Book Archive