scientific article; zbMATH DE number 7278086
From MaRDI portal
Publication:5136303
DOI10.4230/LIPICS.FSTTCS.2017.14zbMATH Open1498.03150MaRDI QIDQ5136303FDOQ5136303
Authors: Olaf Beyersdorff, Luke Hinde, Ján Pich 
Publication date: 25 November 2020
Title of this publication is not available (Why is that?)
Recommendations
- Reasons for hardness in QBF proof systems
- Hardness and optimality in QBF proof systems modulo NP
- A simple proof of QBF hardness
- QBF Resolution Systems and Their Proof Complexities
- Proof complexity of symbolic QBF reasoning
- On QBF Proofs and Preprocessing
- Classes of hard formulas for QBF resolution
- Hard provability logics
- Hard instances of algorithms and proof systems
- Hard instances of algorithms and proof systems
Cites Work
- Resolution for quantified Boolean formulas
- Expansion-based QBF solving versus Q-resolution
- Solving QBF with counterexample guided refinement
- On Unification of QBF Resolution-Based Calculi
- Proof complexity of resolution-based QBF calculi
- Using SAT in QBF
- Title not available (Why is that?)
- Title not available (Why is that?)
- Contributions to the theory of practical quantified Boolean formula solving
- Title not available (Why is that?)
- QBF Resolution Systems and Their Proof Complexities
- Logical foundations of proof complexity
- A Machine-Oriented Logic Based on the Resolution Principle
- Parity, circuits, and the polynomial-time hierarchy
- The relative efficiency of propositional proof systems
- The intractability of resolution
- Towards NP-P via proof complexity and search
- An exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principle
- The Complexity of Propositional Proofs
- Exponential lower bounds for the pigeonhole principle
- An exponential separation between the parity principle and the pigeonhole principle
- Dual weak pigeonhole principle, Boolean complexity, and derandomization
- On the relative complexity of resolution refinements and cutting planes proof systems
- Conformant planning as a case study of incremental QBF solving
- Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
- Lower bounds: from circuits to QBF proof systems
- Proof Complexity Modulo the Polynomial Hierarchy: Understanding Alternation as a Source of Hardness
- Understanding Gentzen and Frege Systems for QBF
- Understanding cutting planes for QBFs
- Q-resolution with generalized axioms
- Long distance Q-resolution with dependency schemes
- Feasible interpolation for QBF resolution calculi
Cited In (11)
- Lower bound techniques for QBF expansion
- Proof complexity of modal resolution
- Reasons for hardness in QBF proof systems
- Hardness and optimality in QBF proof systems modulo NP
- Lower bounds for QCDCL via formula gauge
- How QBF expansion makes strategy extraction hard
- Understanding cutting planes for QBFs
- Characterising tree-like Frege proofs for QBF
- A simple proof of QBF hardness
- Lower bound techniques for QBF proof systems
- Proof complexity modulo the polynomial hierarchy: understanding alternation as a source of hardness
Uses Software
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5136303)
