A note on regular resolution

Abstract

Tseitin [3] and Galil [1] have proven that for infinitely manyn there is a set of clausesS(n) of the propositional calculus of lengthn such that any regular resolution proof ofS(n) produces at least 2^cn distinct new clauses for somec>0. We show that it is possible to obtain a much weaker but still non-polynomial bound of 2^{clog 2} n by a simpler argument.

Zusammenfassung

Tseitin [3] und Galil [1] haben gezeigt, daß es in der Aussagenlogik für unendlich vielen KlausenmengenS(n) der Längen gibt, so daß jeder reguläre Resolutionsbeweis fürS(n) mindestens 2^cn (für einec>0) verschiedene Klausen enthält. Wir geben hier einen einfacheren Beweis für die viel schwächere aber dennoch nichtpolynomiale Schranke 2^{clog 2} n an.