A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses

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

Mathematics Subject Classification ID

Related Items (21)

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

• Coq
• SMT-LIB
• zChaff
• z3
• HOL Light
• veriT
• CVC Lite
• GitHub

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

This page was built for publication: A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses