On Sequent Systems and Resolution for QBFs
On Sequent Systems and Resolution for QBFs
复制标题
关于 QBF 的顺序系统和解析
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Uwe Egly
中科院分区：
文献类型：
--
作者：
Uwe Egly
量化布尔公式通过允许对命题变量进行量化来推广命题公式。我们比较了具有不同量词处理范例的量化布尔公式(QBF)的证明系统，就其允许简洁证明的能力而言。我们分析了由不同的量词规则扩展的无割序列系统，并证明了一些规则比另一些规则更好。
Q-归结是命题归结在QBF上的一个很好的推广，适用于前置合取范式的公式。在Q解析中，不存在特定规则对量词的显式处理。取而代之的是，操作单个子句的forall约简规则检查全局量词前缀。我们证明了在序列系统中有一些公式存在无短路树证明，但对该公式的否定的任何q-分辨反驳都是指数的。
Quantified Boolean formulas generalize propositional formulas by admitting quantifications over propositional variables. We compare proof systems with different quantifier handling paradigms for quantified Boolean formulas (QBFs) with respect to their ability to allow succinct proofs. We analyze cut-free sequent systems extended by different quantifier rules and show that some rules are better than some others.
Q-resolution is an elegant extension of propositional resolution to QBFs and is applicable to formulas in prenex conjunctive normal form. In Q-resolution, there is no explicit handling of quantifiers by specific rules. Instead the forall reduction rule which operates on single clauses inspects the global quantifier prefix. We show that there are classes of formulas for which there are short cut-free tree proofs in a sequent system, but any Q-resolution refutation of the negation of the formula is exponential.