An instantiation scheme for satisfiability modulo theories
From MaRDI portal
Publication:438578
DOI10.1007/s10817-010-9200-3zbMath1430.68401OpenAlexW2041790367MaRDI QIDQ438578
Nicolas Peltier, Mnacho Echenim
Publication date: 31 July 2012
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-010-9200-3
Related Items (3)
Satisfiability Modulo Theories ⋮ Modular instantiation schemes ⋮ Variant-Based Satisfiability in Initial Algebras
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Eliminating dublication with the hyper-linking strategy
- Solving quantified verification conditions using satisfiability modulo theories
- Decidable fragments of many-sorted logic
- Theory decision by decomposition
- A rewriting approach to satisfiability procedures.
- Ordered semantic hyper-linking
- Fourier-Motzkin elimination and its dual
- Engineering DPLL(T) + Saturation
- Simplify: a theorem prover for program checking
- Instantiation of SMT Problems Modulo Integers
- Efficient E-Matching for SMT Solvers
- Automatic Decidability and Combinability Revisited
- Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
- Computer Science Logic
- Automatic Combinability of Rewriting-Based Satisfiability Procedures
- On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- Verification, Model Checking, and Abstract Interpretation
This page was built for publication: An instantiation scheme for satisfiability modulo theories
