Cutting plane versus frege proof systems
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 show: Frege proof systems p-simulate the cutting plane proof system. This strengthens a result in , that extended Frege proof systems (which are believed to be stronger than Frege proof systems) p-simulate the cutting plane proof system. Our proof is based on the techniques introduced in .
KeywordsProof System Propositional Variable Propositional Formula Polynomial Size Pigeonhole Principle
Unable to display preview. Download preview PDF.
- M. Ajtai, The complexity of the pigeonhole principle, Proceedings of the 29th Symposium on foundations of Computer Science (1988) 346–355.Google Scholar
- S. Buss, Polynomial size proofs of the propositional pigeonhole principle, Journ. Symb. Logic 52 (1987) 916–927.Google Scholar
- C.-L. Chang, R.C.-T. Lee, Symbolic logic and mechanical theorem proving, Academic Press (1973).Google Scholar
- P. Clote, Bounded arithmetic and computational complexity, Proceedings Structure in Complexity (1990) 186–199.Google Scholar
- S.A. Cook, R.A. Reckhow, The relative efficiency of propositional proof systems, Journ. Sym. Logic 44 (1979) 36–50.Google Scholar
- J.N. Hooker, Generalized resolution and cutting planes, Annals of Oper. Res. 12 (1988) 217–239.Google Scholar
- P. Pudlak, Ramsey's theorem in bounded arithmetic, Workshop in Comp. Sci. Logic 1990, Springer LNCS, submitted.Google Scholar
- R.M. Smullyan, First-order Logic, Springer Verlag 1968.Google Scholar
- A. Goerdt, Cutting plane versus Frege proof systems, Technical report, University of Duisburg.Google Scholar