Title
Constant-depth Frege systems with counting axioms polynomially simulate Nullstellensatz refutations
Abstract
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 propositional formulas to systems of polynomials. Using our definition of reducibility, most previously studied propositional formulas reduce to their polynomial translations. 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 upper bounds on refutation sizes for certain CNFs in constant-depth Frege with counting axioms systems.
Year
DOI
Venue
2003
10.1145/1131313.1131314
ACM Transactions on Computational Logic (TOCL)
Keywords
DocType
Volume
upper bound
Journal
7
Issue
ISSN
Citations 
2
1529-3785
2
PageRank 
References 
Authors
0.38
24
2
Name
Order
Citations
PageRank
Russell Impagliazzo15444482.13
Nathan Segerlind222311.22