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.
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.