## Abstract

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 language | English (US) |
---|---|

Pages (from-to) | 407-457 |

Number of pages | 51 |

Journal | Computational Complexity |

Volume | 17 |

Issue number | 3 |

DOIs | |

State | Published - Oct 2008 |

Externally published | Yes |

## All Science Journal Classification (ASJC) codes

- Theoretical Computer Science
- General Mathematics
- Computational Theory and Mathematics
- Computational Mathematics

## Keywords

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