Quantifier Instantiation Techniques for Finite Model Finding in SMT
- 1 January 2013
- book chapter
- Published by Springer Nature
- p. 377-391
Abstract
No abstract availableKeywords
This publication has 9 references indexed in Scilit:
- Protocol Proof Checking Simplified with SMT2012
- Extending Sledgehammer with SMT Solvers2011
- Incremental Instance Generation in Local Reasoning2009
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories2009
- The model evolution calculus as a first-order DPLL methodArtificial Intelligence, 2008
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)2008
- Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL2007
- Efficient E-Matching for SMT Solvers2007
- Term Rewriting and All That1998