Quantified Propositional Logspace Reasoning

In this paper, we develop a quantified propositional proof systems that corresponds to logarithmic-space reasoning. We begin by defining a classCNF(2) of quantified formulas that can be evaluated in log space. Then our new proof system GL∗ is defined as G∗1 with cuts restricted to �CNF(2) formulas and no cut formula that is not quantifier free contains a free variable that does not appear in the final formula. To show that GL∗ is strong enough to capture log space reason- ing, we translate theorems of V L into a family of tautologies that have polynomial-size GL∗ proofs. V L is a theory of bounded arithmetic that is known to correspond to logarithmic-space reasoning. To do the trans- lation, we find an appropriate axiomatization of V L, and put V L proofs into a new normal form. To show that GL∗ is not too strong, we prove the soundness of GL∗