On Propositional QBF Expansions and Q-Resolution

DOI10.1007/978-3-642-39071-5_7zbMath1390.03017OpenAlexW45235819MaRDI QIDQ5326454

Mikoláš Janota, João P. Marques-Silva

Publication date: 5 August 2013

Published in: Theory and Applications of Satisfiability Testing – SAT 2013 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-39071-5_7

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)

Related Items

The QBF Gallery: behind the scenes ⋮ Long-distance Q-resolution with dependency schemes ⋮ Soundness of \(\mathcal{Q}\)-resolution with dependency schemes ⋮ Level-ordered \(Q\)-resolution and tree-like \(Q\)-resolution are incomparable ⋮ A Game Characterisation of Tree-like Q-resolution Size ⋮ Lifting QBF Resolution Calculi to DQBF ⋮ Long Distance Q-Resolution with Dependency Schemes ⋮ Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations ⋮ Expansion-based QBF solving versus Q-resolution ⋮ Solving QBF with counterexample guided refinement ⋮ Certified DQBF solving by definition extraction

Uses Software

• DepQBF