Abstract
The cutting plane proof system for proving the unsatisfiability of propositional formulas in conjunctive normalform is based on a natural representation of formulas as systems of integer inequalities. We define a restriction of this system, the cutting plane system with bounded degree of falsity, and show the results: This system p-simulates resolution and has polynomial size proofs for the pigeonhole formulas. The formulas from [ 9] only have superpolynomially long proofs in the system. Our system is the only known system with provably superpolynomial proof size, but polynomial size proofs for the pigeonhole formulas.
Preview
Unable to display preview. Download preview PDF.
References
M. Ajtai, The complexity of the pigeonhole principle, Proceedings of the 29th Symposium on Foundations of Computer Science (1988).
S. Buss, Polynomial size proofs of the propositional pigeonhole principle, Journ. Symb. Logic 52 (1987) pp.916–927.
C.-L. Chang, R.C.-T. Lee, Symbolic Logic and mechanical theorem proving, Academic Press (1973).
P. Clote, Bounded arithmetic and computational complexity, Proceedings Structures in Complexity (1990) pp. 186–199.
W. Cook, C.R. Coullard, G. Turan, On the complexity of cutting plane proofs, Discr. Appl. Math. 18 (1987) pp. 25–38.
S. A. Cook, R.A. Reckhow, The relative efficiency of propositional proof systems, Journ. Sym. Logic 44 (1979) pp. 36–50.
A. Haken, The intractability of resolution, Theor. Comp. Sci. 39 (1985) pp. 297–308.
A. Goerdt, Cutting plane versus Frege proof systems, CSL (1990) LNCS 533, pp. 174–194.
A. Urquhart, Hard examples for resolution, JACM 34 (1) (1987) pp. 209–219.
R.A. Smullyan, First-order Logic, Springer Verlag (1968).
V. Chvatal, Probabilistic methods in graph theory, Annals of Operations Research 1 (1984) pp. 171–182.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Goerdt, A. (1992). The cutting plane proof system with bounded degree of falsity. In: Börger, E., Jäger, G., Kleine Büning, H., Richter, M.M. (eds) Computer Science Logic. CSL 1991. Lecture Notes in Computer Science, vol 626. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0023762
Download citation
DOI: https://doi.org/10.1007/BFb0023762
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55789-0
Online ISBN: 978-3-540-47285-8
eBook Packages: Springer Book Archive