  Quantified Boolean formulas (QBFs) generalize propositional formulas by
admitting quantifications over propositional variables. QBFs can be viewed as
(restricted) formulas of first-order predicate logic and easy translations of
QBFs into first-order formulas exist. We analyze different translations and
show that first-order resolution combined with such translations can
polynomially simulate well-known deduction concepts for QBFs. Furthermore, we
extend QBF calculi by the possibility to instantiate a universal variable by an
existential variable of smaller level. Combining such an enhanced calculus with
the propositional extension rule results in a calculus with a universal
quantifier rule which essentially introduces propositional formulas for
universal variables. In this way, one can mimic a very general quantifier rule
known from sequent systems.
