Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6874144 | Information Processing Letters | 2018 | 7 Pages |
Abstract
In this note we show two results about k-DNF resolution. First we prove that there are CNF formulas which require exponential length refutations in resolution extended with parities of size k, but have polynomial length refutations in k-DNF resolution. Then we show that small proofs in tree-like k-DNF resolution and narrow proofs in dag-like resolution have the same proving power, over CNFs. This latter result is clearly implicit in KrajÃÄek (1994) [24] but this direct proof is focused on resolution and provides information about refutation width.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Massimo Lauria,