Resolution over linear equations and multilinear proofs

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


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



    Upload a copy of this work     Papers currently archived: 92,873

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

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.


Added to PP

24 (#675,416)

6 months
10 (#306,545)

Historical graph of downloads
How can I increase my downloads?