Canonization for disjoint unions of theories

DOI10.1016/J.IC.2004.11.001zbMATH Open1078.68138OpenAlexW2013378402MaRDI QIDQ2486580FDOQ2486580

Authors Sava Krstić, Sylvain Conchon

Publication date 5 August 2005

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ic.2004.11.001

zbMATH Keywords

decision proceduresShostak's method

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Canonization for disjoint unions of theories.
• scientific article; zbMATH DE number 2090060
• Theoretical Aspects of Computing - ICTAC 2004
• Unification in the union of disjoint equational theories: Combining decision procedures
• Combination techniques and decision problems for disunification

Cites work

• scientific article; zbMATH DE number 1140674 (Why is no real title available?)
• scientific article; zbMATH DE number 1956606 (Why is no real title available?)
• scientific article; zbMATH DE number 2086593 (Why is no real title available?)
• scientific article; zbMATH DE number 2086596 (Why is no real title available?)
• scientific article; zbMATH DE number 2090060 (Why is no real title available?)
• scientific article; zbMATH DE number 2090127 (Why is no real title available?)
• scientific article; zbMATH DE number 2090311 (Why is no real title available?)
• Combining decision procedures.
• Deciding Combinations of Theories
• Deciding the word problem in the union of equational theories.
• On Shostak's decision procedure for combinations of theories
• Simplification by Cooperating Decision Procedures
• Superposition modulo a Shostak theory.
• The join of equational theories
• Unions of non-disjoint theories and combinations of satisfiability procedures

Cited in

(9)

• \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
• Solutions of functional equations in Shostak theories
• Canonized Rewriting and Ground AC Completion Modulo Shostak Theories
• Canonization for disjoint unions of theories.
• Building Extended Canonizers by Graph-Based Deduction
• Theoretical Aspects of Computing - ICTAC 2004
• Politeness for the theory of algebraic datatypes
• Revisiting the canonicity of canonical triangulations
• Polite combination of algebraic datatypes

Describes a project that uses

Uses Software

• PVS

This page was built for publication: Canonization for disjoint unions of theories

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