The strength of multilinear proofs
The paper is a contribution to the study of proof complexity of algebraic proof systems. The authors introduce a semantic refutation system fMC (formula multilinear calculus) that is similar to the polynomial calculus (PC) except that lines of the proof are represented by multilinear arithmetic formulas. It is shown in the paper that depth-2 fMC simulates PC and resolution, as well as their common generalization PCR (polynomial calculus with resolution), that there are polynomial-size depth-3 fMC refutations over fields of characteristic 0 of the functional pigeonhole principle, and polynomial-size depth-3 fMC refutations over fields including a primitive \(p\)th root of unity of Tseitin mod-\(p\) tautologies. The last two results imply exponential speed-up of fMC over PCR and bounded-depth Frege. A general form of the simulation of PCR by fMC also gives an interesting result that certain proof complexity lower bounds imply circuit lower bounds (namely, any explicit super-polynomial separation between proof systems similar to fMC but operating with general arithmetic circuits, or multilinear circuits, respectively, implies a super-polynomial lower bound on multilinear circuit size of an explicit sequence of multilinear polynomials).
- The proof complexity of linear algebra
- Proof of Rueppel's linear complexity conjecture (Corresp.)
- Nullstellensatz-proofs for multiplier verification
- A sharp threshold in proof complexity
- On the complexity of cutting-plane proofs
- Resolution over linear equations and multilinear proofs
- Complexity of Null- and Positivstellensatz proofs
- On proving parameterized size lower bounds for multilinear algebraic models
- On proving parameterized size lower bounds for multilinear algebraic models
- Proof Complexity and the Kneser-Lovász Theorem
- Algebraic proof systems over formulas.
- Characterizing propositional proofs as noncommutative formulas
- scientific article; zbMATH DE number 7471587 (Why is no real title available?)
- The surprising power of constant depth algebraic proofs
- Proof complexity lower bounds from algebraic circuit complexity
- Algebraic proofs over noncommutative formulas
- Resolution over linear equations and multilinear proofs
This page was built for publication: The strength of multilinear proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1024659)
