Logic in Computer Science (LICS 1992)

Paper: Cutting planes and constant depth Frege proofs (at LICS 1992)

Authors: Clote, P.

Abstract

The cutting planes refutation system for propositional logic is an extension of resolution and is based on showing the nonexistence of solutions for families of integer linear inequalities. The author defines a modified system of cutting planes with limited extension and shows that this system can polynomially simulate constant-depth Frege proof systems. The principal tool to establish this result is an effective version of cut elimination for modified cutting planes with limited extension. Thus, within a polynomial factor, one can simulate classical propositional logic proofs using modus ponens by refutation-style proofs, provided the formula depth is bounded by a constant. Propositional versions of the Paris-Harrington theorem, Kanamori-McAloon theorem, and variants are proposed as possible candidates for combinatorial tautologies that may require exponential-size cutting planes and Frege proofs

BibTeX

  @InProceedings{Clote-Cuttingplanesandcon,
    author = 	 {Clote, P.},
    title = 	 {Cutting planes and constant depth Frege proofs},
    booktitle =  {Proceedings of the Seventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1992},
    year =	 1992,
    editor =	 {Andre Scedrov},
    month =	 {June}, 
    pages =      {296--307},
    location =   {Santa Cruz, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }