Quantified Boolean Formulas (QBF) and their proof complexity are not as well understood as
propositional formulas, yet remain an area of interest due to their relation to QBF solving. Proof
systems for QBF provide a theoretical underpinning for the performance of these solvers. We define
a novel calculus IR-calc, which enables unification of the principal existing resolution-based QBF
calculi and applies to the more powerful Dependency QBF (DQBF).
We completely reveal the relative power of important QBF resolution systems, settling in
particular the relationship between the two different types of resolution-based QBF calculi. The
most challenging part of this comparison is to exhibit hard formulas that underlie the exponential
separations of the proof systems. In contrast to classical proof complexity we are currently short
of lower bound techniques for QBF proof systems. To this end we exhibit a new proof technique
for showing lower bounds in QBF proof systems based on strategy extraction. We also find that
the classical lower bound techniques of the prover-delayer game and feasible interpolation can be
lifted to a QBF setting and provide new lower bounds.
We investigate more powerful proof systems such as extended resolution and Frege systems. We
define and investigate new QBF proof systems that mix propositional rules with a reduction rule,
we find the strategy extraction technique also works and directly lifts lower bounds from circuit
complexity. Such a direct transfer from circuit to proof complexity lower bounds has often been
postulated, but had not been formally established for propositional proof systems prior to this work.
This leads to strong lower bounds for restricted versions of QBF Frege, in particular an exponential
lower bound for QBF Frege systems operating with AC0[p] circuits. In contrast, any non-trivial
lower bound for propositional AC0[p]-Frege constitutes a major open problem.