We continue a study initiated by Krajicek of a Resolution-like proof system working with clauses of linear inequalities, R(CP). For all proof systems of this kind Krajicek proved an exponential lower bound that depends on the maximal absolute value of coefficients in the given proof and the maximal clause width. ... more >>>

We prove that the Cutting Plane proof system based on Gomory-Chvatal cuts polynomially simulates the lift-and-project system with integer coefficients written in unary. The restriction on coefficients can be omitted when using Krajicek's cut-free Gentzen-style extension of both systems. We also prove that Tseitin tautologies have short proofs in this ... more >>>