Space Complexity in Propositional Calculus
Michael Alekhnovich, Eli Ben‐Sasson, Alexander Alexandrovich Razborov, Avi Wigderson · SIAM Journal on Computing · 2000
We study space complexity in the framework of propositional proofs. We consider a natural model analogous to Turing machines with a read-only input tape and such popular propositional proof systems as resolution, polynomial calculus, and Frege systems. We propose two different space measures, corresponding to the maximal number of bits, and clauses/monomials that need to be kept in the memory simultaneously. We prove a number of lower and upper bounds in these models, as well as some structural results concerning the clause space for resolution and Frege systems.