For every n >0, we show the existence of a CNF tautology over O(n^2) variables of width O(\log n) such that it has a Polynomial Calculus Resolution refutation over \{0,1\} variables of size O(n^3polylog(n)) but any Polynomial Calculus refutation over \{+1,-1\} variables requires size 2^{\Omega(n)}. This shows that Polynomial Calculus ... more >>>

In this paper, we obtain new size lower bounds for proofs in the
Polynomial Calculus (PC) proof system, in two different settings.

1. When the Boolean variables are encoded using \pm 1 (as opposed
to 0,1): We establish a lifting theorem using an asymmetric gadget
G, showing ... more >>>

For every prime p > 0, every n > 0 and ? = O(logn), we show the existence
of an unsatisfiable system of polynomial equations over O(n log n) variables of degree O(log n) such that any Polynomial Calculus refutation over F_p with M extension variables, each depending on at ... more >>>

A major open problem in proof complexity is to prove super-polynomial lower bounds for AC^0[p]-Frege proofs. This system is the analog of AC^0[p], the class of bounded depth circuits with prime modular counting gates. Despite strong lower bounds for this class dating back thirty years (Razborov, '86 and Smolensky, '87), ... more >>>