Standard

Algebraic proof systems over formulas. / Grigoriev, Dima; Hirsch, Edward A.

In: Theoretical Computer Science, Vol. 303, No. 1, 28.06.2003, p. 83-102.

Research output: Contribution to journal › Conference article › peer-review

Harvard

Grigoriev, D & Hirsch, EA 2003, 'Algebraic proof systems over formulas', Theoretical Computer Science, vol. 303, no. 1, pp. 83-102. https://doi.org/10.1016/S0304-3975(02)00446-2

APA

Grigoriev, D., & Hirsch, E. A. (2003). Algebraic proof systems over formulas. Theoretical Computer Science, 303(1), 83-102. https://doi.org/10.1016/S0304-3975(02)00446-2

Vancouver

Grigoriev D, Hirsch EA. Algebraic proof systems over formulas. Theoretical Computer Science. 2003 Jun 28;303(1):83-102. https://doi.org/10.1016/S0304-3975(02)00446-2

Author

Grigoriev, Dima ; Hirsch, Edward A. / Algebraic proof systems over formulas. In: Theoretical Computer Science. 2003 ; Vol. 303, No. 1. pp. 83-102.

BibTeX

@article{e8d38ccf9e63436ea56540d6e33f7634,
title = "Algebraic proof systems over formulas",
abstract = "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.",
keywords = "Algebraic propositional proof systems, Frege systems",
author = "Dima Grigoriev and Hirsch, {Edward A.}",
year = "2003",
month = jun,
day = "28",
doi = "10.1016/S0304-3975(02)00446-2",
language = "English",
volume = "303",
pages = "83--102",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",
number = "1",
note = "Logic and Complexity in Computer Science ; Conference date: 03-09-2001 Through 05-09-2001",

}

RIS

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 - Conference article

AN - SCOPUS:0038378813

VL - 303

SP - 83

EP - 102

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 1

T2 - Logic and Complexity in Computer Science

Y2 - 3 September 2001 through 5 September 2001

ER -

ID: 49828883