Proof systems for quantified Boolean formulas (QBFs) provide a theoretical underpinning for the performance of important
QBF solvers. However, the proof complexity of these proof systems is currently not well understood and in particular
lower bound techniques are missing. In this paper we exhibit a new and elegant proof technique ... more >>>

Recently Beyersdorff, Bonacina, and Chew (ITCS'16) introduced a natural class of Frege systems for quantified Boolean formulas (QBF) and showed strong lower bounds for restricted versions of these systems. Here we provide a comprehensive analysis of the new extended Frege system from Beyersdorff et al., denoted EF+$\forall$red, which is a ... more >>>

Quantified Boolean Formulas (QBFs) extend propositional formulas with Boolean quantifiers. Working with QBF differs from propositional logic in its quantifier handling, but as propositional satisfiability (SAT) is a subproblem of QBF, all SAT hardness in solving and proof complexity transfers to QBF. This makes it difficult to analyse efforts dealing ... more >>>

In this paper we show that the QBF proof checking format QRAT (Quantified Resolution Asymmetric Tautologies) by Heule, Biere and Seidl cannot have polynomial-time strategy extraction unless P=PSPACE. In our proof, the crucial property that makes strategy extraction PSPACE-hard for this proof format is universal expansion, even expansion on a ... more >>>

We advance the theory of QBF proof systems by showing the first simulation of the universal checking format QRAT by a theory-friendly system. We show that the sequent system G fully p-simulates QRAT, including the Extended Universal Reduction (EUR) rule which was recently used to show QRAT does not ... more >>>

We pioneer a new technique that allows us to prove a multitude of previously open simulations in QBF proof complexity. In particular, we show that extended QBF Frege p-simulates clausal proof systems such as IR-Calculus, IRM-Calculus, Long-Distance Q-Resolution, and Merge Resolution.
These results are obtained by taking a technique ... more >>>

The proof complexity of Quantified Boolean Formulas (QBF) relates to both QBF solving and OBF certification. One method to p-simulate a QBF proof system is by formalising the soundness of its strategy extraction in propositional logic. In this work we illustrate how to use extended QBF Frege to simulate LD-Q(Drrs)-Res, ... more >>>