__
Revision #1 to TR07-010 | 19th January 2007 00:00
__
#### Improved Lower Bounds for tree-like Resolution over Linear Inequalities Revision of: TR07-010

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

__
TR07-010 | 4th January 2007 00:00
__

#### Improved Lower Bounds for Resolution over Linear Inequalities

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