Over the years, proof systems for propositional satisfiability (SAT)
have been extensively studied. Recently, proof systems for
quantified Boolean formulas (QBFs) have also been gaining attention.
Q-resolution is a calculus enabling producing proofs from
DPLL-based QBF solvers. While DPLL has become a dominating technique
for SAT, QBF has been tackled by other complementary and competitive
approaches. One of these approaches is based on expanding variables
until the formula contains only one type of quantifier; upon which a
SAT solver is invoked. This approach motivates the theoretical
analysis carried out in this paper. We focus on a two phase proof system,
which expands the formula in the first phase and applies propositional
resolution in the second. Fragments of this proof system are defined and
compared to Q-resolution.