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

decision procedureequivalence classlinear arithmeticproof checkerprototype verification system

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

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

Cited in

(19)

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

Describes a project that uses

Uses Software

• PVS
• NQTHM
• EVES

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)