کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
435467 689909 2016 19 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Soundness of Q-resolution with dependency schemes
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Soundness of Q-resolution with dependency schemes
چکیده انگلیسی

Q-resolution and Q-term resolution are proof systems for quantified Boolean formulas (QBFs). We introduce generalizations of these proof systems named Q(D)Q(D)-resolution and Q(D)Q(D)-term resolution. Q(D)Q(D)-resolution and Q(D)Q(D)-term resolution are parameterized by a dependency scheme D   and use more powerful ∀-reduction and ∃-reduction rules, respectively. We show soundness of these systems for particular dependency schemes: we prove (1) soundness of Q(D)Q(D)-resolution parameterized by the reflexive resolution-path dependency scheme, and (2) soundness of Q(D)Q(D)-term resolution parameterized by the resolution-path dependency scheme. These results entail soundness of the proof systems used for certificate generation in the state-of-the-art solver DepQBF.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Theoretical Computer Science - Volume 612, 25 January 2016, Pages 83–101
نویسندگان
, ,