期刊名称:Electronic Colloquium on Computational Complexity
印刷版ISSN:1433-8092
出版年度:2001
卷号:2001
出版社:Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要: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.
关键词:Frege systems , Nullstellensatz , Polynomial Calculus , Propositional Proof System