期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：1997
卷号：1997
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：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 ,
no set of size less than 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).
