Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR01-011 | 21st January 2001 00:00

Algebraic proof systems over formulas


Authors: Dima Grigoriev, Edward Hirsch
Publication: 8th February 2001 19:32
Downloads: 3922


We introduce two algebraic propositional proof systems F-NS
and F-PC. 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 F-NS provide an exponential
separation between this system and Polynomial Calculus.

We prove that F-NS (and hence F-PC) polynomially simulates
Frege systems, and that the constant-depth version of F-PC over
finite field polynomially simulates constant-depth Frege systems
with modular counting. We also present a short constant-depth
F-PC (in fact, F-NS) proof of the propositional pigeon-hole
principle. Finally, we introduce several extensions of our
systems and pose numerous open questions.

ISSN 1433-8092 | Imprint