Boolean programs and quantified propositional proof systems

We introduce the notion of Boolean programs, which provide more concise de-scriptions of Boolean functions than Boolean circuits. We characterize nonuni-form PSPACE in terms of polynomial size families of Boolean programs. We then show how to use Boolean programs to witness quantifiers in the subsystems G1 and G 1 of the proof system G for the quantified propositional calculus.