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

We call a pseudorandom generator $G_n:\{0,1\}^n\to \{0,1\}^m$ {\em hard} for a propositional proof system $P$ if $P$ can not efficiently prove the (properly encoded) statement $G_n(x_1,\ldots,x_n)\neq b$ for {\em any} string $b\in\{0,1\}^m$. We consider a variety of ``combinatorial'' pseudorandom generators inspired by the Nisan-Wigderson generator on the one hand, and ... more >>>

We introduce two algebraic propositional proof systems F-NS and F-PC. The main difference of our systems from (customary) Nullstellensatz and Polynomial Calculus is that the polynomials are represented as arbitrary formulas (rather than sums of monomials). Short proofs of Tseitin's tautologies in the constant-depth version of F-NS provide an exponential ... more >>>

We introduce an algebraic proof system that manipulates multilinear arithmetic formulas. We show that this proof system is fairly strong, even when restricted to multilinear arithmetic formulas of a very small depth. Specifically, we show the following: 1. Algebraic proofs manipulating depth 2 multilinear arithmetic formulas polynomially simulate Resolution, Polynomial ... more >>>

We introduce an algebraic proof system Pcrk, which combines together {\em Polynomial Calculus} (Pc) and {\em $k$-DNF Resolution} (Resk). This is a natural generalization to Resk of the well-known {\em Polynomial Calculus with Resolution} (Pcr) system which combines together Pc and Resolution. We study the complexity of proofs in such ... more >>>

We study the space required by Polynomial Calculus refutations of random $k$-CNFs. We are interested in how many monomials one needs to keep in memory to carry on a refutation. More precisely we show that for $k \geq 4$ a refutation of a random $k$-CNF of $\Delta n$ clauses and ... more >>>