Soundness of Q-resolution with dependency schemes.
Theoretical Computer Science(2016)
摘要
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 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)-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.
更多查看译文
关键词
Quantified Boolean formulas,QBF,Q-resolution,Dependency schemes
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络