Combination techniques for non-disjoint equational theories
From MaRDI portal
Publication:5210778
DOI10.1007/3-540-58156-1_19zbMath1433.68544OpenAlexW1526479036MaRDI QIDQ5210778
Christophe Ringeissen, Eric Domenjoud, Francis Klay
Publication date: 21 January 2020
Published in: Automated Deduction — CADE-12 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/3-540-58156-1_19
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
Non-disjoint combined unification and closure by equational paramodulation ⋮ Combination of constraint solving techniques: An algebraic point of view ⋮ A new combination procedure for the word problem that generalizes fusion decidability results in modal logics ⋮ Unification algorithms cannot be combined in polynomial time ⋮ A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method ⋮ Unions of non-disjoint theories and combinations of satisfiability procedures ⋮ Unification algorithms cannot be combined in polynomial time.
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Combination techniques and decision problems for disunification
- Modularity of simple termination of term rewriting systems with shared constructors
- Complete sets of transformations for general E-unification
- Recursive Unsolvability of a problem of Thue
- Combining matching algorithms: The regular case