Validating QBF Validity in HOL4
From MaRDI portal
Recommendations
- Validating QBF invalidity in HOL4
- Proving Valid Quantified Boolean Formulas in HOL Light
- scientific article; zbMATH DE number 5542982
- Efficiently checking propositional refutations in HOL theorem provers
- QMaude: quantitative specification and verification in rewriting logic
- Logic for Programming, Artificial Intelligence, and Reasoning
- A First Step Towards a Unified Proof Checker for QBF
- Solving quantified verification conditions using satisfiability modulo theories
Cites work
- A Brief Overview of HOL4
- A Brief Overview of PVS
- A First Step Towards a Unified Proof Checker for QBF
- A formulation of the simple theory of types
- A Short Presentation of Coq
- Combining Coq and Gappa for Certifying Floating-Point Programs
- Computer Aided Verification
- Edinburgh LCF. A mechanized logic of computation
- Efficiently checking propositional refutations in HOL theorem provers
- Evaluating and certifying QBFs: a comparison of state-of-the-art tools
- Fast LCF-Style Proof Reconstruction for Z3
- scientific article; zbMATH DE number 1670733 (Why is no real title available?)
- scientific article; zbMATH DE number 5542982 (Why is no real title available?)
- scientific article; zbMATH DE number 3560737 (Why is no real title available?)
- scientific article; zbMATH DE number 1950260 (Why is no real title available?)
- scientific article; zbMATH DE number 2090293 (Why is no real title available?)
- Learning to integrate deduction and search in reasoning about quantified Boolean formulas
- Logic versus Approximation
- MetiTarski: An automatic theorem prover for real-valued special functions
- Report of the third QBF solvers evaluation
- Resolution for quantified Boolean formulas
- The Isabelle Framework
- Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Translating higher-order clauses to first-order clauses
- Validating QBF invalidity in HOL4
Cited in
(8)- Polynomial-time validation of QCDCL certificates
- Unified QBF certification and its applications
- Proving Valid Quantified Boolean Formulas in HOL Light
- Evaluating and certifying QBFs: a comparison of state-of-the-art tools
- scientific article; zbMATH DE number 5542982 (Why is no real title available?)
- Validating QBF invalidity in HOL4
- Never trust your solver: certification for SAT and QBF
- CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver
Describes a project that uses
Uses Software
This page was built for publication: Validating QBF Validity in HOL4
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3088005)
