The Proof Complexity of Polynomial Identities

Devising an efficient deterministic – or even a nondeterministic sub-exponential time – algorithm for testing polynomial identities is a fundamental problem in algebraic complexity and complexity at large. Motivated by this problem, as well as by results from proof complexity, we investigate the complexity of proving polynomial identities. To this end, we study a class of equational proof systems, of varying strength, operating with polynomial identities written as arithmetic formulas over a given ring. A proof in these systems establishes that two arithmetic formulas compute the same polynomial, and consists of a sequence of equations between polynomials, written as arithmetic formulas, where each equation in the sequence is derived from previous equations by means of the polynomial-ring axioms. We establish the first non-trivial upper and lower bounds on the size of equational proofs of polynomial identities, as follows: 1) Polynomial-size upper bounds on equational proofs of ...

• Type: Conference
• Year: 2009
• Where: COCO
• Authors: Pavel Hrubes, Iddo Tzameret
• Keywords: COCO 2009, Equational Proofs, Lower Bounds, Polynomial Identities, Theoretical Computer Science