The strength of multilinear proofs

Ran Raz, Iddo Tzameret

Research output: Contribution to journalArticlepeer-review

9 Scopus citations


We introduce an algebraic proof system that manipulates multilinear arithmetic formulas. We show that this proof system is fairly strong, even when restricted to multilinear arithmetic formulas of a very small depth. Specifically, we show the following: 1. Algebraic proofs manipulating depth 2 multilinear arithmetic formulas polynomially simulate Resolution, Polynomial Calculus (PC) and Polynomial Calculus with Resolution (PCR) proofs; 2. Polynomial size proofs manipulating depth 3 multilinear arithmetic formulas for the functional pigeonhole principle; 3. Polynomial size proofs manipulating depth 3 multilinear arithmetic formulas for Tseitin's graph tautologies. By known lower bounds, this demonstrates that algebraic proof systems manipulating depth 3 multilinear formulas are strictly stronger than Resolution, PC and PCR, and have an exponential gap over bounded-depth Frege for both the functional pigeonhole principle and Tseitin's graph tautologies. We also illustrate a connection between lower bounds on multilinear proofs and lower bounds on multilinear circuits. In particular, we show that (an explicit) super-polynomial size separation between proofs manipulating general arithmetic circuits and proofs manipulating multilinear circuits implies a super-polynomial size lower bound on multilinear circuits for an explicit family of polynomials.

Original languageEnglish (US)
Pages (from-to)407-457
Number of pages51
JournalComputational Complexity
Issue number3
StatePublished - Oct 2008
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Mathematics(all)
  • Computational Theory and Mathematics
  • Computational Mathematics


  • Multilinear arithmetic formulas
  • Polynomial calculus
  • Proof complexity
  • Propositional pigeonhole principle
  • Tseitin tautologies


Dive into the research topics of 'The strength of multilinear proofs'. Together they form a unique fingerprint.

Cite this