Several calculi for quantified Boolean formulas (QBFs) exist, but
relations between them are not yet fully understood.
This paper defines a novel calculus, which is resolution-based and
enables unification of the principal existing resolution-based QBF
calculi, namely Q-resolution, long-distance Q-resolution and the expansion-based
calculus $\forall$Exp+Res. All these calculi play an important role in QBF solving.
This paper shows simulation results for the new calculus and some of its
variants. Further, we demonstrate how to obtain winning strategies for the universal
player from proofs in the calculus.
We believe that this new proof system opens new avenues for further
research and provides a suitable formalism for certification of existing solvers.

Improved presentation of the calculi as well as increased flexibility thereof.

Several calculi for quantified Boolean formulas (QBFs) exist, but
relations between them are not yet fully understood.
This paper defines a novel calculus, which is resolution-based and
enables unification of the principal existing resolution-based QBF
calculi, namely Q-resolution, long-distance Q-resolution and the expansion-based
calculus $\forall$Exp+Res. All these calculi play an important role in QBF solving.
This paper shows simulation results for the new calculus and some of its
variants. Further, we demonstrate how to obtain winning strategies for the universal
player from proofs in the calculus.
We believe that this new proof system opens new avenues for further
research and provides a suitable formalism for certification of existing solvers.