Lower Bounds for cutting planes proofs with small coefficients

Journal of Symbolic Logic 62 (3):708-728 (1997)

Abstract
We consider small-weight Cutting Planes (CP * ) proofs; that is, Cutting Planes (CP) proofs with coefficients up to $\operatorname{Poly}(n)$ . We use the well known lower bounds for monotone complexity to prove an exponential lower bound for the length of CP * proofs, for a family of tautologies based on the clique function. Because Resolution is a special case of small-weight CP, our method also gives a new and simpler exponential lower bound for Resolution. We also prove the following two theorems: (1) Tree-like CP * proofs cannot polynomially simulate non-tree-like CP * proofs. (2) Tree-like (CP * proofs and Bounded-depth-Frege proofs cannot polynomially simulate each other. Our proofs also work for some generalizations of the CP * proof system. In particular, they work for CP * with a deduction rule, and also for any proof system that allows any formula with small communication complexity, and any set of sound rules of inference
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2307/2275569
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,955
Through your library

References found in this work BETA

Pool Resolution is NP-Hard to Recognize.Samuel R. Buss - 2009 - Archive for Mathematical Logic 48 (8):793-798.

Add more references

Citations of this work BETA

Resolution Over Linear Equations and Multilinear Proofs.Ran Raz & Iddo Tzameret - 2008 - Annals of Pure and Applied Logic 155 (3):194-224.

Add more citations

Similar books and articles

Analytics

Added to PP index
2009-01-28

Total views
34 ( #277,087 of 2,310,280 )

Recent downloads (6 months)
4 ( #264,424 of 2,310,280 )

How can I increase my downloads?

Downloads

My notes

Sign in to use this feature