TR01-011 Authors: Dima Grigoriev, Edward Hirsch

Publication: 8th February 2001 19:32

Downloads: 1811

Keywords:

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.