Validating QBF Validity in HOL4

DOI10.1007/978-3-642-22863-6_14zbMATH Open1342.68290OpenAlexW4232871528MaRDI QIDQ3088005FDOQ3088005

Authors: 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

Recommendations

• Validating QBF invalidity in HOL4
• Proving Valid Quantified Boolean Formulas in HOL Light
• scientific article
• 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

Mathematics Subject Classification ID

Cites Work

• The Isabelle Framework
• Theory and Applications of Satisfiability Testing
• A Brief Overview of PVS
• A Brief Overview of HOL4
• Edinburgh LCF. A mechanized logic of computation
• Title not available (Why is that?)
• Resolution for quantified Boolean formulas
• Title not available (Why is that?)
• Title not available (Why is that?)
• A formulation of the simple theory of types
• Efficiently checking propositional refutations in HOL theorem provers
• Translating higher-order clauses to first-order clauses
• A Short Presentation of Coq
• Title not available (Why is that?)
• Fast LCF-Style Proof Reconstruction for Z3
• 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
• Combining Coq and Gappa for Certifying Floating-Point Programs
• Computer Aided Verification
• Theory and Applications of Satisfiability Testing
• A First Step Towards a Unified Proof Checker for QBF
• Report of the third QBF solvers evaluation
• Title not available (Why is that?)
• Evaluating and certifying QBFs: a comparison of state-of-the-art tools
• Logic versus Approximation
• Learning to integrate deduction and search in reasoning about quantified Boolean formulas
• Validating QBF invalidity in HOL4

Cited In (4)

• Title not available (Why is that?)
• Evaluating and certifying QBFs: a comparison of state-of-the-art tools
• Validating QBF invalidity in HOL4
• Proving Valid Quantified Boolean Formulas in HOL Light

Uses Software

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

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)