التفاصيل البيبلوغرافية
| العنوان: |
Relating size and width in variants of Q-resolution. |
| المؤلفون: |
Clymo, Judith1, Beyersdorff, Olaf1,2 o.beyersdorff@leeds.ac.uk |
| المصدر: |
Information Processing Letters. Oct2018, Vol. 138, p1-6. 6p. |
| مصطلحات موضوعية: |
BOOLEAN algebra, MATHEMATICAL proofs, MATHEMATICAL formulas, COMPUTATIONAL complexity, CALCULUS |
| مستخلص: |
In their influential paper ‘Short proofs are narrow – resolution made simple’ [3] , Ben-Sasson and Wigderson introduced a crucial tool for proving lower bounds on the lengths of proofs in the resolution calculus. Over a decade later their technique for showing lower bounds on the size of proofs, by examining the width of all possible proofs, remains one of the most effective lower bound techniques in propositional proof complexity. We continue the investigation begun in [6] into the application of this technique to proof systems for quantified Boolean formulas. We demonstrate a relationship between the size of proofs in level-ordered Q-Resolution and the width of proofs in Q-Resolution. In general, however, the picture is not positive, and for most stronger systems based on Q-Resolution, the size-width relation of [3] fails, answering an open question from [6] . [ABSTRACT FROM AUTHOR] |
|
Copyright of Information Processing Letters is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites or posted to a listserv without the copyright holder's express written permission. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) |
| قاعدة البيانات: |
Business Source Index |
