Resolution over linear equations and multilinear proofs

DOI10.1016/j.apal.2008.04.001zbMath1161.03034MaRDI QIDQ952492

Iddo Tzameret, Ran Raz

Publication date: 12 November 2008

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2008.04.001

zbMATH Keywords

cutting planes; resolution; algebraic proof systems; proof complexity; feasible interpolation; multilinear proofs

Mathematics Subject Classification ID

03F20: Complexity of proofs

Related Items

Randomized feasible interpolation and monotone circuits with a local oracle, Characterizing Propositional Proofs as Noncommutative Formulas, Unnamed Item, Unnamed Item, Algebraic proofs over noncommutative formulas, Resolution with counting: dag-like lower bounds and different moduli, On conversions from CNF to ANF, Resolution over linear equations modulo two

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The strength of multilinear proofs
• The intractability of resolution
• The monotone circuit complexity of Boolean functions
• Lower bounds for the weak pigeonhole principle and random formulas beyond resolution
• Several notes on the power of Gomory-Chvátal cuts
• On the weak pigeonhole principle
• Space Complexity in Propositional Calculus
• Monotone Circuits for Connectivity Require Super-Logarithmic Depth
• Improved Lower Bounds for Tree-Like Resolution over Linear Inequalities
• The relative efficiency of propositional proof systems
• Discretely ordered modules as a first-order extension of the cutting planes proof system
• Lower bounds to the size of constant-depth propositional proofs
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Lower bounds for cutting planes proofs with small coefficients
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic
• An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams
• Multi-linear formulas for permanent and determinant are of super-polynomial size
• Linear gaps between degrees for the polynomial calculus modulo distinct primes
• Depth-3 arithmetic circuits over fields of characteristic zero