A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
From MaRDI portal
Publication:3100209
DOI10.1007/978-3-642-25379-9_12zbMath1350.68223OpenAlexW81349459MaRDI QIDQ3100209
Benjamin Werner, Chantal Keller, Michaël Armand, Laurent Théry, Benjamin Grégoire, Germain Faure
Publication date: 22 November 2011
Published in: Certified Programs and Proofs (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-25379-9_12
Related Items
Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver, Semi-intelligible Isar proofs from machine-generated proofs, Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs, Practical Proof Search for Coq by Type Inhabitation, Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3, Hammer for Coq: automation for dependent type theory, SMT-based generation of symbolic automata, FoCaLiZe and Dedukti to the rescue for proof interoperability, A semantic framework for proof evidence, SMT proof checking using a logical framework, \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML, A formalization of convex polyhedra based on the simplex method, Extensible and Efficient Automation Through Reflective Tactics, Scalable fine-grained proofs for formula processing, Reliable reconstruction of fine-grained proofs in a proof assistant, A Survey of Satisfiability Modulo Theory, Modular SMT Proofs for Fast Reflexive Checking Inside Coq, Tactics for Reasoning Modulo AC in Coq, SAT-Enhanced Mizar Proof Checking, Flexible proof production in an industrial-strength SMT solver, Extending Sledgehammer with SMT solvers
Uses Software
Cites Work
- Unnamed Item
- Interactive theorem proving. First international conference, ITP 2010, Edinburgh, UK, July 11--14, 2010. Proceedings
- Autarkic computations in formal proofs
- Solving SAT and SAT Modulo Theories
- Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
- Extending Coq with Imperative Features and Its Application to SAT Verification
- Fast LCF-Style Proof Reconstruction for Z3
- Tools and Algorithms for the Construction and Analysis of Systems
