Combination techniques for non-disjoint equational theories

DOI10.1007/3-540-58156-1_19MaRDI QIDQ5210778zbMATH OpenOpenAlexFDO

Authors Eric Domenjoud, Francis Klay, Christophe Ringeissen

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• An improved general E-unification method
• Combination techniques and decision problems for disunification
• Combining matching algorithms: The regular case
• Complete sets of transformations for general E-unification
• scientific article; zbMATH DE number 1324441 (Why is no real title available?)
• scientific article; zbMATH DE number 1348479 (Why is no real title available?)
• scientific article; zbMATH DE number 1414317 (Why is no real title available?)
• Modularity of simple termination of term rewriting systems with shared constructors
• Recursive unsolvability of a problem of Thue

Cited in

(7)

• Unions of non-disjoint theories and combinations of satisfiability procedures
• Unification algorithms cannot be combined in polynomial time.
• A new combination procedure for the word problem that generalizes fusion decidability results in modal logics
• Unification algorithms cannot be combined in polynomial time
• Combination of constraint solving techniques: An algebraic point of view
• A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method
• Non-disjoint combined unification and closure by equational paramodulation

This page was built for publication: Combination techniques for non-disjoint equational theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5210778)