A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method
From MaRDI portal
Publication:5234683
DOI10.1007/3-540-63104-6_3zbMath1430.03036OpenAlexW1830416912MaRDI QIDQ5234683
Publication date: 1 October 2019
Published in: Automated Deduction—CADE-14 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/3-540-63104-6_3
Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)
Related Items
Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties, A new combination procedure for the word problem that generalizes fusion decidability results in modal logics, Combining Non-Stably Infinite Theories, Connection calculus theorem proving with multiple built-in theories, A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method, Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols, Unions of non-disjoint theories and combinations of satisfiability procedures
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unification in a combination of arbitrary disjoint equational theories
- Counterexamples to termination for the direct sum of term rewriting systems
- Complexity, convexity and combinations of theories
- Combining symbolic constraint solvers on algebraic domains
- Unions of non-disjoint theories and combinations of satisfiability procedures
- Fast Decision Procedures Based on Congruence Closure
- Simplification by Cooperating Decision Procedures
- An Efficient Unification Algorithm
- Combining matching algorithms: The regular case
- Combination techniques for non-disjoint equational theories
- A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method
- On the Church-Rosser property for the direct sum of term rewriting systems
- A Machine-Oriented Logic Based on the Resolution Principle
