On Unification of QBF Resolution-Based Calculi

DOI10.1007/978-3-662-44465-8_8zbMath1426.68283OpenAlexW1525848078WikidataQ59900282 ScholiaQ59900282MaRDI QIDQ2922598

Mikoláš Janota, Leroy Chew, Olaf Beyersdorff

Publication date: 14 October 2014

Published in: Mathematical Foundations of Computer Science 2014 (Search for Journal in Brave)

Full work available at URL: http://eprints.whiterose.ac.uk/80488/1/paper.pdf

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

The QBF Gallery: behind the scenes, Feasible Interpolation for QBF Resolution Calculi, Unnamed Item, A simple proof of QBF hardness, Lower Bound Techniques for QBF Proof Systems, Long-distance Q-resolution with dependency schemes, Unnamed Item, Soundness of \(\mathcal{Q}\)-resolution with dependency schemes, Never trust your solver: certification for SAT and QBF, A game characterisation of tree-like Q-resolution size, Towards Uniform Certification in QBF, Lower bound techniques for QBF expansion, Characterising tree-like Frege proofs for QBF, Unnamed Item, Understanding cutting planes for QBFs, A Game Characterisation of Tree-like Q-resolution Size, Incremental Determinization, On Stronger Calculi for QBFs, Q-Resolution with Generalized Axioms, Lifting QBF Resolution Calculi to DQBF, Long Distance Q-Resolution with Dependency Schemes, Dual proof generation for quantified Boolean formulas with a BDD-based solver, Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations, Unnamed Item, Reinterpreting dependency schemes: soundness meets incompleteness in DQBF, Unnamed Item, Unnamed Item, Solving QBF with counterexample guided refinement