The strength of multilinear proofs (Q1024659): Difference between revisions

From MaRDI portal
Importer (talk | contribs)
Created a new Item
 
Added link to MaRDI item.
links / mardi / namelinks / mardi / name
 

Revision as of 22:06, 30 January 2024

scientific article
Language Label Description Also known as
English
The strength of multilinear proofs
scientific article

    Statements

    The strength of multilinear proofs (English)
    0 references
    0 references
    0 references
    17 June 2009
    0 references
    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).
    0 references
    proof complexity
    0 references
    multilinear arithmetical formulas
    0 references
    polynomial calculus
    0 references
    pigeonhole principle
    0 references
    Tseitin tautologies
    0 references

    Identifiers