Resolution over linear equations and multilinear proofs

Annals of Pure and Applied Logic 155 (3):194-224 (2008)

Abstract
We develop and study the complexity of propositional proof systems of varying strength extending resolution by allowing it to operate with disjunctions of linear equations instead of clauses. We demonstrate polynomial-size refutations for hard tautologies like the pigeonhole principle, Tseitin graph tautologies and the clique-coloring tautologies in these proof systems. Using interpolation we establish an exponential-size lower bound on refutations in a certain, considerably strong, fragment of resolution over linear equations, as well as a general polynomial upper bound on interpolants in this fragment.We then apply these results to extend and improve previous results on multilinear proofs , as studied in [Ran Raz, Iddo Tzameret, The strength of multilinear proofs. Comput. Complexity ]. Specifically, we show the following:• Proofs operating with depth-3 multilinear formulas polynomially simulate a certain, considerably strong, fragment of resolution over linear equations.• Proofs operating with depth-3 multilinear formulas admit polynomial-size refutations of the pigeonhole principle and Tseitin graph tautologies. The former improve over a previous result that established small multilinear proofs only for the functional pigeonhole principle. The latter are different from previous proofs, and apply to multilinear proofs of Tseitin mod p graph tautologies over any field of characteristic 0. We conclude by connecting resolution over linear equations with extensions of the cutting planes proof system
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/j.apal.2008.04.001
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 48,902
Through your library

References found in this work BETA

View all 7 references / Add more references

Citations of this work BETA

Add more citations

Similar books and articles

The Depth of Resolution Proofs.Alasdair Urquhart - 2011 - Studia Logica 99 (1-3):349-364.
Resolution Calculus for the First Order Linear Logic.Grigori Mints - 1993 - Journal of Logic, Language and Information 2 (1):59-83.
A Parallel Game Semantics for Linear Logic.Stefano Baratella & Stefano Berardi - 1997 - Archive for Mathematical Logic 36 (3):189-217.
Equality of Proofs for Linear Equality.Kosta Došen & Zoran Petrić - 2008 - Archive for Mathematical Logic 47 (6):549-565.
The Complexity of Resolution Refinements.Joshua Buresh-Oppenheim & Toniann Pitassi - 2007 - Journal of Symbolic Logic 72 (4):1336 - 1352.
Cutting Planes, Connectivity, and Threshold Logic.Samuel R. Buss & Peter Clote - 1996 - Archive for Mathematical Logic 35 (1):33-62.
Maxwell Equations—The One-Photon Quantum Equation.Alexander Gersten - 2001 - Foundations of Physics 31 (8):1211-1231.

Analytics

Added to PP index
2013-12-26

Total views
8 ( #891,956 of 2,309,728 )

Recent downloads (6 months)
3 ( #353,970 of 2,309,728 )

How can I increase my downloads?

Downloads

My notes

Sign in to use this feature