Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations

We prove an exponential lower bound on the length of cutting plane proofs. The proof uses an extension of a lower bound for monotone circuits to circuits which compute with real numbers and use nondecreasing functions as gates. The latter result is of independent interest, since, in particular, it implies an exponential lower bound for some arithmetic circuits. 1 Introduction The problem of proving lower bounds on the length of propositional proofs is generally recognized as one of the most important problems in logic and complexity theory. Its importance stems from its relation to independence results in bounded arithmetic and to the problem NP ? = coNP, see [17]. There is no general technique available, which would work for all propositional proof systems (this is needed to prove that NP 6= coNP). Therefore we are trying to extend our current methods to stronger and stronger systems. The first important step was Haken's exponential lower bound on the length of resolution proofs [..