Cutting plane versus frege proof systems

  • Andreas Goerdt
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 533)


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 [5], 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 [2].


Proof System Propositional Variable Propositional Formula Polynomial Size Pigeonhole Principle 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    M. Ajtai, The complexity of the pigeonhole principle, Proceedings of the 29th Symposium on foundations of Computer Science (1988) 346–355.Google Scholar
  2. [2]
    S. Buss, Polynomial size proofs of the propositional pigeonhole principle, Journ. Symb. Logic 52 (1987) 916–927.Google Scholar
  3. [3]
    C.-L. Chang, R.C.-T. Lee, Symbolic logic and mechanical theorem proving, Academic Press (1973).Google Scholar
  4. [4]
    P. Clote, Bounded arithmetic and computational complexity, Proceedings Structure in Complexity (1990) 186–199.Google Scholar
  5. [5]
    W. Cook, C.R. Coullard, G. Turan, On the complexity of cutting plane proofs, Discr. Appl. Math. 18 (1987) 25–38.CrossRefGoogle Scholar
  6. [6]
    S.A. Cook, R.A. Reckhow, The relative efficiency of propositional proof systems, Journ. Sym. Logic 44 (1979) 36–50.Google Scholar
  7. [7]
    A. Haken, The intractability of resolution, Theor. Comp. Sci. 39 (1985) 297–308.CrossRefGoogle Scholar
  8. [8]
    J.N. Hooker, Generalized resolution and cutting planes, Annals of Oper. Res. 12 (1988) 217–239.Google Scholar
  9. [9]
    B. Krishnamurthy, Short proofs for tricky formulas, Acta Informatica 22 (1985) 253–275.CrossRefGoogle Scholar
  10. [10]
    P. Pudlak, Ramsey's theorem in bounded arithmetic, Workshop in Comp. Sci. Logic 1990, Springer LNCS, submitted.Google Scholar
  11. [11]
    R.M. Smullyan, First-order Logic, Springer Verlag 1968.Google Scholar
  12. [12]
    A. Goerdt, Cutting plane versus Frege proof systems, Technical report, University of Duisburg.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • Andreas Goerdt
    • 1
  1. 1.Fachbereich Mathematik/Praktische InformatikUniversität-GH-DuisburgDuisburgGermany

Personalised recommendations