Deciding the Word Problem in the Union of Equational Theories
- 1 November 2002
- journal article
- Published by Elsevier in Information and Computation
- Vol. 178 (2) , 346-390
- https://doi.org/10.1006/inco.2001.3118
Abstract
No abstract availableKeywords
This publication has 21 references indexed in Scilit:
- Combination of constraint solvers for free and quasi-free structuresTheoretical Computer Science, 1998
- Combining Symbolic Constraint Solvers on Algebraic DomainsJournal of Symbolic Computation, 1994
- Unification in a combination of arbitrary disjoint equational theoriesJournal of Symbolic Computation, 1989
- Counterexamples to termination for the direct sum of term rewriting systemsInformation Processing Letters, 1987
- On the Church-Rosser property for the direct sum of term rewriting systemsJournal of the ACM, 1987
- Completion of a Set of Rules Modulo a Set of EquationsSIAM Journal on Computing, 1986
- An Efficient Unification AlgorithmACM Transactions on Programming Languages and Systems, 1982
- Fast Decision Procedures Based on Congruence ClosureJournal of the ACM, 1980
- Simplification by Cooperating Decision ProceduresACM Transactions on Programming Languages and Systems, 1979
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965