Validating QBF Validity in HOL4
From MaRDI portal
Publication:3088005
DOI10.1007/978-3-642-22863-6_14zbMath1342.68290OpenAlexW4232871528MaRDI QIDQ3088005
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_14
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings
- MetiTarski: An automatic theorem prover for real-valued special functions
- Efficiently checking propositional refutations in HOL theorem provers
- Edinburgh LCF. A mechanized logic of computation
- Resolution for quantified Boolean formulas
- Translating higher-order clauses to first-order clauses
- Evaluating and certifying QBFs: A comparison of state-of-the-art tools
- A Short Presentation of Coq
- A Brief Overview of PVS
- A Brief Overview of HOL4
- The Isabelle Framework
- A First Step Towards a Unified Proof Checker for QBF
- Combining Coq and Gappa for Certifying Floating-Point Programs
- Learning to Integrate Deduction and Search in Reasoning about Quantified Boolean Formulas
- Computer Aided Verification
- Theory and Applications of Satisfiability Testing
- Logic versus Approximation
- Theory and Applications of Satisfiability Testing
- Fast LCF-Style Proof Reconstruction for Z3
- Validating QBF Invalidity in HOL4
- A formulation of the simple theory of types
This page was built for publication: Validating QBF Validity in HOL4
