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

We prove that Polynomial Calculus and Polynomial Calculus with Resolution are not automatizable, unless W[P]-hard problems are fixed parameter tractable by one-side error randomized algorithms. This extends to Polynomial Calculus the analogous result obtained for Resolution by Alekhnovich and Razborov (SIAM J. Computing, 38(4), 2008). 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 >>>