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 for showing lower bounds
in QBF proof systems based on strategy extraction. This technique provides a direct transfer of circuit lower bounds to
lengths of proofs lower bounds. We use our method to show the hardness of a natural class of parity formulas for
Q-resolution. Variants of the formulas are hard for even stronger systems as long-distance and universal Q-resolution.
With a completely different lower bound argument we show the hardness of the prominent formulas of Kleine Büning et
al. for the strong expansion-based calculus IR-calc, thus also confirming the hardness of the formulas for Q-resolution.
Our lower bounds imply new exponential separations between two different types of resolution-based QBF calculi: proof
systems for DPLL-based solvers (Q-resolution, long-distance Q-resolution) and proof systems for expansion-based solvers
($\forall$Exp+Res and its generalizations IR-calc and IRM-calc). The relations between proof systems from the two
different classes were not known before.