Article ID Journal Published Year Pages File Type
4662474 Annals of Pure and Applied Logic 2006 8 Pages PDF
Abstract

We prove that the Cutting Plane proof system based on Gomory–Chvátal cuts polynomially simulates the lift-and-project system with integer coefficients written in unary. The restriction on the coefficients can be omitted when using Krajíček’s cut-free Gentzen-style extension of both systems. We also prove that Tseitin tautologies have short proofs in this extension (of any of these systems and with any coefficients).

Related Topics
Physical Sciences and Engineering Mathematics Logic