Abstract:
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. In this paper we improve this lower bound. For tree-like R(CP)-like proof systems we remove a dependence on the maximal absolute value of coefficients. Proof follows from an upper bound on the real communication complexity of a polyhedra.

Abstract:
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. In this paper we improve his lower bound for two restricted versions of R(CP)-like proof systems. For tree-like R(CP)-like proof systems we remove a dependence on the maximal absolute value of coefficients. Proof follows from an upper bound on the real communication complexity of a polyhedra. For R(CP) we remove a dependence on the maximal clause width. Proof follows from the fact that in R(CP) at each step we modify at most one inequality in a clause. Hence, we can use information about other inequalities from previous steps and do not need to check all inequalities in the clause.