Modular instantiation schemes

DOI10.1016/J.IPL.2011.07.003MaRDI QIDQ1944184zbMATH OpenOpenAlexFDO

Authors Mnacho Echenim, Nicolas Peltier

Publication date 4 April 2013

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ipl.2011.07.003

zbMATH Keywords

automatic theorem provingcombination problemsinstantiation-based methodsSMT

Mathematics Subject Classification ID

Recommendations

• An instantiation scheme for satisfiability modulo theories
• Instantiation schemes for nested theories
• Theory Instantiation
• Instantiation of SMT problems modulo integers
• Automatic decidability and combinability

Cites work

• An instantiation scheme for satisfiability modulo theories
• Automated Deduction – CADE-20
• Combining nonstably infinite theories
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Decidable fragments of many-sorted logic
• Decision procedures for extensions of the theory of arrays
• scientific article; zbMATH DE number 1140674 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• Ordered semantic hyper-linking
• Satisfiability modulo theories: an appetizer
• Verification, Model Checking, and Abstract Interpretation

Cited in

(5)

• Modular invariants for layered object structures
• Instantiation schemes for nested theories
• Instantiation of SMT problems modulo integers
• Incremental modular decomposition
• An instantiation scheme for satisfiability modulo theories

This page was built for publication: Modular instantiation schemes

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