Cutting planes, connectivity, and threshold logic

Archive for Mathematical Logic 35 (1):33-62 (1996)
  Copy   BIBTEX


Originating from work in operations research the cutting plane refutation systemCP is an extension of resolution, where unsatisfiable propositional logic formulas in conjunctive normal form are recognized by showing the non-existence of boolean solutions to associated families of linear inequalities. Polynomial sizeCP proofs are given for the undirecteds-t connectivity principle. The subsystemsCP q ofCP, forq≥2, are shown to be polynomially equivalent toCP, thus answering problem 19 from the list of open problems of [8]. We present a normal form theorem forCP 2-proofs and thereby for arbitraryCP-proofs. As a corollary, we show that the coefficients and constant terms in arbitrary cutting plane proofs may be exponentially bounded by the number of steps in the proof, at the cost of an at most polynomial increase in the number of steps in the proof. The extensionCPLE +, introduced in [9] and there shown top-simulate Frege systems, is proved to be polynomially equivalent to Frege systems. Lastly, since linear inequalities are related to threshold gates, we introduce a new threshold logic and prove a completeness theorem



    Upload a copy of this work     Papers currently archived: 92,100

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Some remarks on lengths of propositional proofs.Samuel R. Buss - 1995 - Archive for Mathematical Logic 34 (6):377-394.
A note on propositional proof complexity of some Ramsey-type statements.Jan Krajíček - 2011 - Archive for Mathematical Logic 50 (1-2):245-255.
Bounded arithmetic, propositional logic, and complexity theory.Jan Krajíček - 1995 - New York, NY, USA: Cambridge University Press.
Implicit Proofs.Jan Krajíček - 2004 - Journal of Symbolic Logic 69 (2):387 - 397.
Light affine lambda calculus and polynomial time strong normalization.Kazushige Terui - 2007 - Archive for Mathematical Logic 46 (3-4):253-280.
Uniqueness of normal proofs in implicational intuitionistic logic.Takahito Aoto - 1999 - Journal of Logic, Language and Information 8 (2):217-242.


Added to PP

54 (#296,486)

6 months
5 (#644,465)

Historical graph of downloads
How can I increase my downloads?