[Zurück]


Zeitschriftenartikel:

F. Slivovsky, S. Szeider:
"Soundness of Q-resolution with dependency schemes";
Theoretical Computer Science, 612 (2016), S. 83 - 101.



Kurzfassung englisch:
Q-resolution and Q-term resolution are proof systems for quantified Boolean formulas (QBFs). We introduce generalizations of these proof systems named Q(D)-resolution and Q(D)-term resolution. Q(D)-resolution and Q(D)-term resolution are parameterized by a dependency scheme Dand 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)-resolution parameterized by the reflexive resolution-path dependency scheme, and (2)soundness of 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.


"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.1016/j.tcs.2015.10.020

Elektronische Version der Publikation:
http://publik.tuwien.ac.at/files/publik_253433.pdf


Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.