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

Journal of Symbolic Logic 63 (4):1582-1596 (1998)
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. 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)
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2307/2586668
 Save to my reading list
Follow the author(s)
My bibliography
Export citation
Find it on Scholar
Edit this record
Mark as duplicate
Revision history
Request removal from index
Download options
Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 25,767
Through your library
References found in this work BETA
Quantifier Elimination for Modules with Scalar Variables.Lou van den Dries & Jan Holly - 1992 - Annals of Pure and Applied Logic 57 (2):161-179.

Add more references

Citations of this work BETA
Several Notes on the Power of Gomory–Chvátal Cuts.Edward A. Hirsch & Arist Kojevnikov - 2006 - Annals of Pure and Applied Logic 141 (3):429-436.
Resolution Over Linear Equations and Multilinear Proofs.Ran Raz & Iddo Tzameret - 2008 - Annals of Pure and Applied Logic 155 (3):194-224.

Add more citations

Similar books and articles

Monthly downloads

Added to index


Total downloads

3 ( #678,551 of 2,146,897 )

Recent downloads (6 months)

1 ( #385,700 of 2,146,897 )

How can I increase my downloads?

My notes
Sign in to use this feature

There  are no threads in this forum
Nothing in this forum yet.

Other forums