  We show that constant-depth Frege systems with counting axioms modulo $m$
polynomially simulate Nullstellensatz refutations modulo $m$. Central to this
is a new definition of reducibility from formulas to systems of polynomials
with the property that, for most previously studied translations of formulas to
systems of polynomials, a formula reduces to its translation. When combined
with a previous result of the authors, this establishes the first size
separation between Nullstellensatz and polynomial calculus refutations. We also
obtain new, small refutations for certain CNFs by constant-depth Frege systems
with counting axioms.
