On Shostak's decision procedure for combinations of theories

DOI10.1007/3-540-61511-3_107zbMATH Open1415.03019OpenAlexW1546619436MaRDI QIDQ4647541FDOQ4647541

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

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

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)

Cites Work

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

Cited In (19)

• Title not available (Why is that?)
• Canonization for disjoint unions of theories
• Conditional congruence closure over uninterpreted and interpreted symbols
• Title not available (Why is that?)
• Constraint contextual rewriting.
• Title not available (Why is that?)
• Title not available (Why is that?)
• Programmed strategies for program verification
• \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
• On quasitautologies
• Title not available (Why is that?)
• Combining decision procedures.
• Title not available (Why is that?)
• 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
• Deciding Combinations of Theories

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)