Michael Soltys - Boolean programs and quantified propositional proof systems

My talk is going to be based on the following article: Boolean Programs and Quantified Propositional Proof Systems, which I coauthor-ed with Steven Cook, and which is going to appear this Fall in the Bulletin of the Section of Logic.

In this article we introduce the notion of Boolean programs, which provide more concise descriptions of Boolean functions than Boolean circuits. We characterize nonuniform PSPACE in terms of polynomial size families of Boolean programs. We then show how to use Boolean programs to witness quantifiers in the subsystems G₁ and G₁^* of the proof system G for the quantified propositional calculus.