__Journal article:__

** Samuel R. Buss and Peter Clote.
"Cutting planes, connectivity and threshold logic."
Archive for Mathematical Logic 35 (1996) 33-63.**

** Download article: postscript or PDF. **

** Abstract: **Originating from work in operations
research the cutting plane refutation system $CP$ 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 $CP$ proofs are given for the undirected $s$-$t$
connectivity principle. The subsystems $CP_q$ of $CP$, for $q\ge 2$, are shown to be
polynomially equivalent to $CP$, thus answering problem~$19$ from the list of open
problems of \cite{clotekrajicek}. We present a normal form theorem for $CP_2$-proofs and
thereby for arbitrary $CP$-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 $CPLE^+$, introduced in \cite{clote10} and there
shown to $p$-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.