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 (28)

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

This page was built for publication: On Unification of QBF Resolution-Based Calculi