__
TR97-007 | 21st February 1997 00:00
__

#### Exponential Lower Bounds for Semantic Resolution

**Abstract:**

In a semantic resolution proof we operate with clauses only

but allow {\em arbitrary} rules of inference:

C_1 C_2 ... C_m

__________________

C

Consistency is the only requirement. We prove a very simple

exponential lower bound for the size of bounded fanin semantic

resolution proofs of a general {\em Hitting Set Principle} stating

that, for any set system with hitting set number $\tau$,

no set of size less than $\tau$ can be a hitting set.

The pigeonhole principle and known blocking principles for

finite (affine and projective) planes are special cases of this

general principle. The lower bounds argument is essentially the

same argument given by Beame and Pittasi (1996) for the case of

(standard) Resolution, which in turn simplifies earlier arguments

due to Haken (1985).