caa a22 4500 388038934 CHVBK 20180307125015.0 cr unu---uuuuu 161130e199812 xx s 000 0 eng 10.2307/2586668 doi S0022481200014432 pii (NATIONALLICENCE)cambridge-10.2307/2586668 Krajíček Jan Mathematical Institute, and Institute of Computer Science, Academy of Sciences, Prague Mathematical Institute, Oxford University, 24-29 St. Giles', Oxford, OX1 3LB, Great Britain. E-mail: krajicek@math.cas.cz Discretely ordered modules as a first-order extension of the cutting planes proof system [Elektronische Daten] [Jan Krajíček] 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 ai · xi ≥ b (xi 's variables, ai '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. The proof relies on a universal interpolation theorem for semantic derivations [16, Theorem 5.1]. LK(CP) 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(M) for any discretely ordered module M (e.g., LK(Z) extends LK(CP)). 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 (suitable) solution would allow to improve the monotone interpolation theorem and the lower bound for R(CP). Copyright © Association for Symbolic Logic 1998 The Journal of Symbolic Logic Cambridge University Press 63/4(1998-12), 1582-1596 0022-4812 63:4<1582 1998 63 JSL https://doi.org/10.2307/2586668 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.2307/2586668 text/html Onlinezugriff via DOI NATIONALLICENCE 100 1- Krajíček Jan Mathematical Institute, and Institute of Computer Science, Academy of Sciences, Prague Mathematical Institute, Oxford University, 24-29 St. Giles', Oxford, OX1 3LB, Great Britain. E-mail: krajicek@math.cas.cz NATIONALLICENCE 773 0- The Journal of Symbolic Logic Cambridge University Press 63/4(1998-12), 1582-1596 0022-4812 63:4<1582 1998 63 JSL CC0 http://creativecommons.org/publicdomain/zero/1.0 nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-cambridge