On Shostak's decision procedure for combinations of theories

DOI10.1007/3-540-61511-3_107zbMath1415.03019OpenAlexW1546619436MaRDI QIDQ4647541

David Cyrluk, Natarajan Shankar, Patrick D. 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

linear arithmeticequivalence classprototype verification systemdecision procedureproof checker

Mathematics Subject Classification ID

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

Related Items

Constraint contextual rewriting., On quasitautologies, Conditional congruence closure over uninterpreted and interpreted symbols, Up-To Techniques for Weighted Systems, Canonization for disjoint unions of theories, A practical integration of first-order reasoning and decision procedures, Combination of convex theories: modularity, deduction completeness, and explanation, Programmed Strategies for Program Verification

Uses Software

• PVS
• NQTHM
• EVES

Cites Work

• Unnamed Item
• Unnamed Item
• VDM '91. Formal software development methods. Vol. 2: Tutorials. 4th international symposium of VDM Europe, Noordwijkerhout, the Netherlands, October 21-25, 1991. Proceedings
• Deciding Combinations of Theories
• Fast Decision Procedures Based on Congruence Closure
• Simplification by Cooperating Decision Procedures
• Variations on the Common Subexpression Problem
• An algorithm for reasoning about equality