Discretely ordered modules as a first-order extension of the cutting planes proof system

E-ISSN： 1943-5886|63|4|1582-1596

ISSN： 0022-4812

Source： The Journal of Symbolic Logic, Vol.63, Iss.4, 1998-12, pp. : 1582-1596

Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.

Previous Menu Next

Abstract

We define a first-order extension LK(CP) of the cutting planes proof system CP as the first-order sequent calculus LK whose atomic formulas are CP-inequalities ∑_i a_i · x_i ≥ b (x_i 's variables, a_i 's and b constants). We prove an interpolation theorem for LK(CP) yielding as a corollary a conditional lower bound for LK(CP)-proofs. For a subsystem R(CP) of LK(CP), essentially resolution working with clauses formed by CP-inequalities, we prove a monotone interpolation theorem obtaining thus an unconditional lower bound (depending on the maximum size of coefficients in proofs and on the maximum number of CP-inequalities in clauses). We also give an interpolation theorem for polynomial calculus working with sparse polynomials.