On Shostak's decision procedure for combinations of theories

DOI10.1007/3-540-61511-3_107MaRDI QIDQ4647541zbMATH OpenOpenAlexFDO

Authors David Cyrluk, Natarajan Shankar, P. Lincoln

Publication date 15 January 2019

Published in Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-61511-3_107

zbMATH Keywords

equivalence classprototype verification systemdecision procedurelinear arithmeticproof checker

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Combined logics (03B62)

Recommendations

• scientific article; zbMATH DE number 2090060
• Combining decision procedures.
• Strategies for combining decision procedures
• scientific article; zbMATH DE number 1956606
• Deciding Combinations of Theories

Cites work

• scientific article; zbMATH DE number 193479 (Why is no real title available?)
• scientific article; zbMATH DE number 194550 (Why is no real title available?)
• An algorithm for reasoning about equality
• Deciding Combinations of Theories
• Fast Decision Procedures Based on Congruence Closure
• Simplification by Cooperating Decision Procedures
• VDM '91. Formal software development methods. Vol. 2: Tutorials. 4th international symposium of VDM Europe, Noordwijkerhout, the Netherlands, October 21-25, 1991. Proceedings
• Variations on the Common Subexpression Problem

Cited in

(19)

• Deciding Combinations of Theories
• scientific article; zbMATH DE number 2090312 (Why is no real title available?)
• Canonization for disjoint unions of theories
• Conditional congruence closure over uninterpreted and interpreted symbols
• scientific article; zbMATH DE number 2090084 (Why is no real title available?)
• Constraint contextual rewriting.
• Programmed strategies for program verification
• scientific article; zbMATH DE number 2086596 (Why is no real title available?)
• scientific article; zbMATH DE number 2090311 (Why is no real title available?)
• \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
• On quasitautologies
• scientific article; zbMATH DE number 2090060 (Why is no real title available?)
• Combining decision procedures.
• scientific article; zbMATH DE number 1956606 (Why is no real title available?)
• A practical integration of first-order reasoning and decision procedures
• Combination of convex theories: modularity, deduction completeness, and explanation
• Cover Algorithms and Their Combination
• An efficient Nelson-Oppen decision procedure for difference constraints over rationals
• Up-To Techniques for Weighted Systems

Describes a project that uses

Uses Software

• EVES
• NQTHM
• PVS

This page was built for publication: On Shostak's decision procedure for combinations of theories

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