David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Ezio Di Nucci
Jack Alan Reynolds
Learn more about PhilPapers
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)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
Lou van den Dries & Jan Holly (1992). Quantifier Elimination for Modules with Scalar Variables. Annals of Pure and Applied Logic 57 (2):161-179.
Citations of this work BETA
Edward A. Hirsch & Arist Kojevnikov (2006). Several Notes on the Power of Gomory–Chvátal Cuts. Annals of Pure and Applied Logic 141 (3):429-436.
Ran Raz & Iddo Tzameret (2008). Resolution Over Linear Equations and Multilinear Proofs. Annals of Pure and Applied Logic 155 (3):194-224.
Similar books and articles
Melvin Fitting (1999). A Simple Propositional S5 Tableau System. Annals of Pure and Applied Logic 96 (1-3):107-115.
Maria Bonet, Toniann Pitassi & Ran Raz (1997). Lower Bounds for Cutting Planes Proofs with Small Coefficients. Journal of Symbolic Logic 62 (3):708-728.
Hiroakira Ono (1986). Craig's Interpolation Theorem for the Intuitionistic Logic and its Extensions—a Semantical Approach. Studia Logica 45 (1):19 - 33.
Pavel Pudlák (1997). Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations. Journal of Symbolic Logic 62 (3):981-998.
Gerard R. Renardel de Lavalette (2008). Interpolation in Computing Science: The Semantics of Modularization. Synthese 164 (3):437-450.
Gerard R. Renardel De Lavalette (2008). Interpolation in Computing Science: The Semantics of Modularization. Synthese 164 (3):437 - 450.
Martin Otto (2000). An Interpolation Theorem. Bulletin of Symbolic Logic 6 (4):447-462.
Ursula Gropp (1988). Coinductive Formulas and a Many-Sorted Interpolation Theorem. Journal of Symbolic Logic 53 (3):937-960.
Solomon Feferman (2008). Harmonious Logic: Craig's Interpolation Theorem and Its Descendants. Synthese 164 (3):341 - 357.
Jan Krajíček (1997). Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic. Journal of Symbolic Logic 62 (2):457-486.
Added to index2009-01-28
Total downloads3 ( #639,282 of 1,911,608 )
Recent downloads (6 months)1 ( #457,720 of 1,911,608 )
How can I increase my downloads?