Validating QBF Validity in HOL4

DOI10.1007/978-3-642-22863-6_14zbMath1342.68290OpenAlexW4232871528MaRDI QIDQ3088005

Ramana Kumar, Tjark Weber

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

Mathematics Subject Classification ID

Uses Software

• Isabelle
• MetiTarski
• MiniSat
• ML
• PVS
• SMT-LIB
• Gappa
• z3
• HOL
• LCF
• Squolem
• semprop

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