Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR97-007 | 21st February 1997 00:00

Exponential Lower Bounds for Semantic Resolution

RSS-Feed




TR97-007
Authors: Stasys Jukna
Publication: 21st February 1997 17:43
Downloads: 1250
Keywords: 


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



ISSN 1433-8092 | Imprint