Journal article:
Samuel R. Buss, Russell Impagliazzo, Jan Krajicek, Pavel
Pudlak, Alexander Razborov and Jiri Sgall.
"Proof Complexity in Algebraic Systems and Constant Depth Frege
Systems with Modular Counting."
Computational Complexity 6 (1995/1996) 256-298.
Download article: postscript or PDF.
Abstract: We prove a lower bound of the form
$N^{\Omega(1)}$ on the degree of polynomials in a Nullstellensatz refutation of the
$\Count_q$ polynomials over~$\zm$, where $q$ is a prime not dividing $m$. In addition, we
give an explicit construction of a degree $N^{\Omega(1)}$ design for the $\Count_q$
principle over~$\zm$. As a corollary, using \cite{BIKPP} we obtain a lower bound of the
form $2^{N^{\Omega(1)}}$ for the number of formulas in a constant-depth Frege proof of the
modular counting principle $\Count^N_q$ from instances of the counting principle
$\Count^M_m$.
We discuss the polynomial calculus proof system and give a method of
converting tree-like polynomial calculus derivations into low degree Nullstellensatz
derivations.
Further we show that a lower bound for proofs in a bounded depth Frege
system in the language with the modular counting connective $\MOD_p$ follows from a lower
bound on the degree of Nullstellensatz proofs with a constant number of levels of
extension axioms, where the extension axioms comprise a formalization of the approximation
method of Razborov \cite{Ra1}, Smolensky \cite{Sm} (in fact, these two proof systems
are basically equivalent).