Integrating a SAT solver with an LCF-style theorem prover

zbMATH Open1272.68366MaRDI QIDQ2848690FDOQ2848690

Authors: Tjark Weber 

Publication date: 26 September 2013

Full work available at URL: http://www.sciencedirect.com/science/article/pii/S1571066106000089

Recommendations

• Efficiently checking propositional refutations in HOL theorem provers
• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
• Proving Valid Quantified Boolean Formulas in HOL Light
• Extending Sledgehammer with SMT solvers
• Fast LCF-Style Proof Reconstruction for Z3

Mathematics Subject Classification ID

Cited In (12)

• Tools and Algorithms for the Construction and Analysis of Systems
• Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
• Stålmarck's algorithm as a HOL derived rule
• A proof system for graph (non)-isomorphism verification
• Testing a saturation-based theorem prover: experiences and challenges
• Efficiently checking propositional refutations in HOL theorem provers
• Pegasus: sound continuous invariant generation
• SAT-enhanced Mizar proof checking
• Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver
• Incorporating a database of graphs into a proof assistant
• Pegasus: a framework for sound continuous invariant generation
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses

Uses Software

• Isabelle/HOL
• Gandalf

This page was built for publication: Integrating a SAT solver with an LCF-style theorem prover

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