Academy of Sciences of the Czech Rep. Prague, Czech Rep.

Devising an efficient deterministic – or even a non-deterministic sub-exponential time – algorithm for testing polynomial identities is a fundamental problem in alge-braic 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-rin