ECCC-Report TR01-011https://eccc.weizmann.ac.il/report/2001/011Comments and Revisions published for TR01-011en-usThu, 08 Feb 2001 19:32:59 +0200
Paper TR01-011
| Algebraic proof systems over formulas |
Dima Grigoriev,
Edward Hirsch
https://eccc.weizmann.ac.il/report/2001/011We 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.
Thu, 08 Feb 2001 19:32:59 +0200https://eccc.weizmann.ac.il/report/2001/011