Proving Valid Quantified Boolean Formulas in HOL Light
From MaRDI portal
Publication:3088006
DOI10.1007/978-3-642-22863-6_15zbMath1342.68291OpenAlexW152437424MaRDI QIDQ3088006
Publication date: 17 August 2011
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-22863-6_15
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- MetiTarski: An automatic theorem prover for real-valued special functions
- Efficiently checking propositional refutations in HOL theorem provers
- A Skeptic's approach to combining HOL and Maple
- Translating higher-order clauses to first-order clauses
- Evaluating and certifying QBFs: A comparison of state-of-the-art tools
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- A First Step Towards a Unified Proof Checker for QBF
- Towards Self-verification of HOL Light
- Logic versus Approximation
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Fast LCF-Style Proof Reconstruction for Z3
- Validating QBF Invalidity in HOL4
This page was built for publication: Proving Valid Quantified Boolean Formulas in HOL Light
