Cutting plane and Frege proofs
type: Item
instance of: scholarly article
title: Cutting plane and Frege proofs
zbMATH Open document ID: 0835.03024
published in: Information and Computation
publication date: 1996-04-16T00:00:00Z
review text: The cutting plane refutation system CP for classical propositional calculus [see \textit{W. Cook}, \textit{C. R. Coullard} and \textit{Gy. Turan}, Discrete Appl. Math. 18, 25-38 (1987; Zbl 0625.90056)], initially coming from works in operation research, can be considered as an extension of resolution based on showing the non-existence of solutions for families of integer linear inequalities. In this paper the author introduces a modification \(\text{CP}^+\) of the system CP and proves that \(\text{CP}^+\) can polynomially simulate Frege proof systems. An effective cut-elimination theorem for \(\text{CP}^+\) is obtained and a translation of Frege proofs into \(\text{CP}^+\) proofs is described. A propositional formulation of the Paris-Harrington theorem [see \textit{J. Paris} and \textit{L. Harrington}, ``A mathematical incompleteness in Peano arithmetic'', in: Handbook of mathematical logic (J. Barwise, ed.), 1133- 1142 (1977; Zbl 0443.03001)], the Kanamori-McAloon theorem [see \textit{A. Kanamori} and \textit{K. McAloon}, Ann. Pure Appl. Logic 33, 23-41 (1987; Zbl 0627.03041)] and variants are proposed as possible candidates for combinatorial tautologies which may require exponential size cutting plane and Frege proofs.
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 03B05
zbMATH DE Number: 799033
zbMATH Keywords: cutting plane refutation system
zbMATH Keywords: classical propositional calculus
zbMATH Keywords: Frege proof systems
zbMATH Keywords: cut-elimination
zbMATH Keywords: Paris-Harrington theorem
zbMATH Keywords: Kanamori- McAloon theorem
zbMATH Keywords: combinatorial tautologies
author: Peter Clote
reviewed by: Branislav Boričić
MaRDI profile type: Publication
OpenAlex ID: W2026203667
DOI: 10.1006/INCO.1995.1126
description: scientific article; zbMATH DE number 799033