Very recently, Esteban and Toran proposed a convenient definition of space complexity for the most popular propositional proof system, Resolution. Our main goal is to generalize the natural notion of space complexity to stronger propositional proof systems, and research its properties. Besides Resolution, we consider Polynomial Calculus and Frege systems, and we are interested in two different space measures, corresponding to the maximal number of bits, and clauses/monomials that need be kept in the memory simultaneously. We prove a number of lower and upper bounds in these models for such important principles as Pigeonhole principle and Tseitin tautologies, as well as for "universal" tautologies. We also establish some structural results concerning the clause space for Resolution and Frege Systems.
Joint work with M. Alekhnovich, E. Ben-Sasson and A. Wigderson; text of the paper is available at ftp://ftp.eccc.uni-trier.de/pub/eccc/reports/1999/TR99-040/index.html