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)|
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.
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.
Similar books and articles
A Simple Propositional S5 Tableau System.Melvin Fitting - 1999 - Annals of Pure and Applied Logic 96 (1-3):107-115.
Harmonious Logic: Craig's Interpolation Theorem and Its Descendants.Solomon Feferman - 2008 - Synthese 164 (3):341 - 357.
Coinductive Formulas and a Many-Sorted Interpolation Theorem.Ursula Gropp - 1988 - Journal of Symbolic Logic 53 (3):937-960.
Interpolation in Computing Science: The Semantics of Modularization.Gerard R. Renardel De Lavalette - 2008 - Synthese 164 (3):437 - 450.
Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations.Pavel Pudlák - 1997 - Journal of Symbolic Logic 62 (3):981-998.
Lower Bounds for Cutting Planes Proofs with Small Coefficients.Maria Bonet, Toniann Pitassi & Ran Raz - 1997 - Journal of Symbolic Logic 62 (3):708-728.
Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic.Jan Krajíček - 1997 - Journal of Symbolic Logic 62 (2):457-486.
Added to index2009-01-28
Total downloads3 ( #678,551 of 2,146,897 )
Recent downloads (6 months)1 ( #385,700 of 2,146,897 )
How can I increase my downloads?
There are no threads in this forum
Nothing in this forum yet.