TY - JOUR
T1 - Algebraic proof systems over formulas
AU - Grigoriev, Dima
AU - Hirsch, Edward A.
PY - 2003/6/28
Y1 - 2003/6/28
N2 - We introduce two algebraic propositional proof systems ℱ-script N sign script S sign and ℱ-script P sign script C sign. The main difference of our systems from (customary) Nullstellensatz and polynomial calculus is that the polynomials are represented as arbitrary formulas (rather than sums of monomials). Short proofs of Tseitin's tautologies in the constant-depth version of ℱ-script N sign script S sign provide an exponential separation between this system and Polynomial Calculus. We prove that ℱ-script N sign script S sign (and hence ℱ-script P sign script C sign) polynomially simulates Frege systems, and that the constant-depth version of ℱ-script P sign script C sign over finite field polynomially simulates constant-depth Frege systems with modular counting. We also present a short constant-depth ℱ-script P sign script C sign (in fact, ℱ-script N sign script S sign) proof of the propositional pigeon-hole principle. Finally, we introduce several extensions of our systems and pose numerous open questions.
AB - We introduce two algebraic propositional proof systems ℱ-script N sign script S sign and ℱ-script P sign script C sign. The main difference of our systems from (customary) Nullstellensatz and polynomial calculus is that the polynomials are represented as arbitrary formulas (rather than sums of monomials). Short proofs of Tseitin's tautologies in the constant-depth version of ℱ-script N sign script S sign provide an exponential separation between this system and Polynomial Calculus. We prove that ℱ-script N sign script S sign (and hence ℱ-script P sign script C sign) polynomially simulates Frege systems, and that the constant-depth version of ℱ-script P sign script C sign over finite field polynomially simulates constant-depth Frege systems with modular counting. We also present a short constant-depth ℱ-script P sign script C sign (in fact, ℱ-script N sign script S sign) proof of the propositional pigeon-hole principle. Finally, we introduce several extensions of our systems and pose numerous open questions.
KW - Algebraic propositional proof systems
KW - Frege systems
UR - http://www.scopus.com/inward/record.url?scp=0038378813&partnerID=8YFLogxK
U2 - 10.1016/S0304-3975(02)00446-2
DO - 10.1016/S0304-3975(02)00446-2
M3 - ???researchoutput.researchoutputtypes.contributiontojournal.conferencearticle???
AN - SCOPUS:0038378813
SN - 0304-3975
VL - 303
SP - 83
EP - 102
JO - Theoretical Computer Science
JF - Theoretical Computer Science
IS - 1
T2 - Logic and Complexity in Computer Science
Y2 - 3 September 2001 through 5 September 2001
ER -