Affordable Access

Publisher Website

Unrestricted resolution versus N-resolution

Authors
Journal
Theoretical Computer Science
0304-3975
Publisher
Elsevier
Publication Date
Volume
93
Issue
1
Identifiers
DOI: 10.1016/0304-3975(92)90216-3

Abstract

Abstract An N-resolution proof is a resolution proof in which the resolution rule is restricted: one clause to which it is applied must only consist of negative literals. N-resolution is complete (Schöning (1987), p. 109, Stickel (1985), p. 86). We construct an infinite family of propositional formulas and show: These formulas have unrestricted resolution proofs whose length is polynomially bounded in their size. All N-resolution proofs of these formulas are of superpolynomial length.

There are no comments yet on this publication. Be the first to share your thoughts.

Statistics

Seen <100 times
0 Comments