Abstract

We define a first-order extension LK of the cutting planes proof system CP as the first-order sequent calculus LK whose atomic formulas are CP-inequalities $\sum_i a_i \cdot x_i \geq b$. We prove an interpolation theorem for LK yielding as a corollary a conditional lower bound for LK-proofs. For a subsystem R of LK, essentially resolution working with clauses formed by CP- inequalities, we prove a monotone interpolation theorem obtaining thus an unconditional lower bound. We also give an interpolation theorem for polynomial calculus working with sparse polynomials. The proof relies on a universal interpolation theorem for semantic derivations [16, Theorem 5.1]. LK can be viewed as a two-sorted first-order theory of Z considered itself as a discretely ordered Z-module. One sort of variables are module elements, another sort are scalars. The quantification is allowed only over the former sort. We shall give a construction of a theory LK for any discretely ordered module M extends LK). The interpolation theorem generalizes to these theories obtained from discretely ordered Z-modules. We shall also discuss a connection to quantifier elimination for such theories. We formulate a communication complexity problem whose solution would allow to improve the monotone interpolation theorem and the lower bound for R.