  We introduce and investigate symbolic proof systems for Quantified Boolean
Formulas (QBF) operating on Ordered Binary Decision Diagrams (OBDDs). These
systems capture QBF solvers that perform symbolic quantifier elimination, and
as such admit short proofs of formulas of bounded path-width and quantifier
complexity. As a consequence, we obtain exponential separations from standard
clausal proof systems, specifically (long-distance) QU-Resolution and IR-Calc.
  We further develop a lower bound technique for symbolic QBF proof systems
based on strategy extraction that lifts known lower bounds from communication
complexity. This allows us to derive strong lower bounds against symbolic QBF
proof systems that are independent of the variable ordering of the underlying
OBDDs, and that hold even if the proof system is allowed access to an
NP-oracle.
