Integrating a SAT solver with an LCF-style theorem prover

MaRDI QIDQ2848690zbMATH OpenFDO

Authors Tjark Weber

Publication date 26 September 2013

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

Mathematics Subject Classification ID

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

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
• Efficiently checking propositional refutations in HOL theorem provers
• Testing a saturation-based theorem prover: experiences and challenges
• Pegasus: sound continuous invariant generation
• Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver
• SAT-enhanced Mizar proof checking
• Incorporating a database of graphs into a proof assistant
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• Pegasus: a framework for sound continuous invariant generation

Describes a project that uses

Uses Software

• Gandalf
• Isabelle/HOL

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)