Abstract. Originating from work in operations research the cutting plane refutation system is an extension of resolution, where unsatisfiable propositional logic formulas in conjunctive normal form are recognized by showing the non-existence of boolean solutions to associated families of linear inequalities. Polynomial size proofs are given for the undirected - connectivity principle. The subsystems of , for , are shown to be polynomially equivalent to , thus answering problem 19 from the list of open problems of [8]. We present a normal form theorem for -proofs and thereby for arbitrary -proofs. As a corollary, we show that the coefficients and constant terms in arbitrary cutting plane proofs may be exponentially bounded by the number of steps in the proof, at the cost of an at most polynomial increase in the number of steps in the proof. The extension , introduced in [9] and there shown to -simulate Frege systems, is proved to be polynomially equivalent to Frege systems. Lastly, since linear inequalities are related to threshold gates, we introduce a new threshold logic and prove a completeness theorem.