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).
展开▼
机译：在语义解析证明中，我们仅使用子句，但允许{ em任意}推理规则：C_1 C_2 ... C_m __________________ C一致性是唯一要求。我们证明了通用{ em Hitting Set Principle}的有界fanin语义分辨率证明的大小的非常简单的指数下界，该证明指出，对于具有命中集编号的任何集系统，其大小集都不能小于命中集。有限（仿射和射影）平面的鸽眼原理和已知的阻挡原理是该通用原理的特例。对于（标准）分辨率，下界参数与Beame和Pittasi（1996）给出的参数基本相同，这又简化了早因Haken（1985）而提出的参数。
展开▼
