Strategies for combining decision procedures

DOI10.1016/J.TCS.2005.11.025MaRDI QIDQ2368951zbMATH OpenOpenAlexFDO

Authors Sylvain Conchon, Sava Krstić

Publication date 28 April 2006

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2005.11.025

zbMATH Keywords

decision proceduresinference systemsNelson-Oppen combinationShostak's algorithm

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 1956606
• Combining decision procedures.
• Frontiers of Combining Systems
• scientific article; zbMATH DE number 2086596
• Combining Proof-Producing Decision Procedures
• A general setting for flexibly combining and augmenting decision procedures
• Combination techniques and decision problems for disunification
• Combination techniques and decision problems for disunification
• Combining Multiple Heuristics
• scientific article; zbMATH DE number 3976758

Cites work

• Abstract congruence closure
• Canonization for disjoint unions of theories.
• Computer Aided Verification
• Deciding Combinations of Theories
• Fast Decision Procedures Based on Congruence Closure
• scientific article; zbMATH DE number 1722718 (Why is no real title available?)
• scientific article; zbMATH DE number 4047065 (Why is no real title available?)
• scientific article; zbMATH DE number 1231673 (Why is no real title available?)
• scientific article; zbMATH DE number 1140674 (Why is no real title available?)
• scientific article; zbMATH DE number 1140675 (Why is no real title available?)
• scientific article; zbMATH DE number 1980926 (Why is no real title available?)
• scientific article; zbMATH DE number 2043522 (Why is no real title available?)
• scientific article; zbMATH DE number 1798183 (Why is no real title available?)
• scientific article; zbMATH DE number 1931669 (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 1903356 (Why is no real title available?)
• scientific article; zbMATH DE number 1903374 (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?)
• Simplification by Cooperating Decision Procedures

Cited in

(7)

• A general setting for flexibly combining and augmenting decision procedures
• Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
• scientific article; zbMATH DE number 1614688 (Why is no real title available?)
• scientific article; zbMATH DE number 1956606 (Why is no real title available?)
• On Shostak's decision procedure for combinations of theories
• scientific article; zbMATH DE number 2090312 (Why is no real title available?)
• Combining decision procedures.

Describes a project that uses

Uses Software

• Maude
• CVC
• Zapato
• ELAN

This page was built for publication: Strategies for combining decision procedures

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