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