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

Back to Sam Buss's publications page.