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 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.