Electronic Resource
Springer
Computing
26 (1981), S. 87-89
ISSN:
1436-5057
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Description / Table of Contents:
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.
Notes:
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.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF02243428
Permalink
|
Location |
Call Number |
Expected |
Availability |