Lower Bounds for Cutting Planes Proofs with Small Coe cientsMaria
Lower Bounds for Cutting Planes Proofs with Small Coe cientsMaria
复制标题
小系数割平面证明的下界Maria
DOI：
--
复制
发表时间：
1995
期刊：
影响因子：
--
通讯作者：
T. Pitassi
中科院分区：
文献类型：
--
作者：
T. Pitassi
我们考虑小重量切割平面（CP）的证明;即，切割平面（CP）的证明与coeecients到Poly（n）。我们使用众所周知的单调复杂性的下界证明CP证明的长度的指数下界，为一个家庭的重言式的基础上的团函数。由于Resolution是小权CP的一种特殊情况，我们的方法也给出了一个新的和更简单的指数下界的Resolution。我们还证明了以下两个定理：（1）树型CP证明不能多项式模拟非树型CP证明。(2)树型CP证明和有界深度Frege证明不能多项式模拟对方。我们的证明也适用于CP证明系统的一些推广。特别是，它们适用于具有演绎规则的CP，也适用于允许任何具有小通信复杂性的公式和任何合理推理规则集的证明系统。1引言命题证明理论中最基本的问题之一是：如何强大的是一个特定的证明系统？特别是，一个试图给重言式的例子，在系统中没有简短的证明。据信，对于任何怀孕的人来说，
We consider small-weight Cutting Planes (CP) proofs; that is, Cutting Planes (CP) proofs with coeecients up to 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 proof systems that allow any formula with small communication complexity, and any set of sound rules of inference. 1 Introduction One of the most fundamental questions in propositional proof theory is: how strong is a particular proof system? In particular , one tries to give examples of tautologies with no short proofs in the system. It is believed that for any conceiv