Proving Valid Quantified Boolean Formulas in HOL Light

DOI10.1007/978-3-642-22863-6_15MaRDI QIDQ3088006zbMATH OpenOpenAlexFDO

Authors Ondřej Kunčar

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

Mathematics Subject Classification ID

Recommendations

• Validating QBF Validity in HOL4
• Validating QBF invalidity in HOL4
• Mechanising Gödel-Löb provability logic in HOL light
• A satisfiability procedure for quantified Boolean formulae
• scientific article; zbMATH DE number 1471980
• Efficiently checking propositional refutations in HOL theorem provers
• Encoding deductive argumentation in quantified Boolean formulae
• Henkin quantifiers and Boolean formulae: a certification perspective of DQBF

Cites work

• 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 2090293 (Why is no real title available?)
• A First Step Towards a Unified Proof Checker for QBF
• A Skeptic's approach to combining HOL and Maple
• 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
• Logic versus Approximation
• MetiTarski: An automatic theorem prover for real-valued special functions
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Towards Self-verification of HOL Light
• Translating higher-order clauses to first-order clauses
• Validating QBF invalidity in HOL4

Cited in

(7)

• Lemma Mining over HOL Light
• Validating QBF Validity in HOL4
• Steps towards Verified Implementations of HOL Light
• scientific article; zbMATH DE number 7594146 (Why is no real title available?)
• Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
• Integrating a SAT solver with an LCF-style theorem prover
• Validating QBF invalidity in HOL4

Describes a project that uses

Uses Software

• Squolem
• LCF
• HOL Light
• z3
• Metis
• MetiTarski

This page was built for publication: Proving Valid Quantified Boolean Formulas in HOL Light

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3088006)