Understanding Gentzen and Frege Systems for QBF
Understanding Gentzen and Frege Systems for QBF
复制标题
了解 QBF 的 Gentzen 和 Frege 系统
DOI：
10.1145/2933575.2933597
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Beyersdorff O
中科院分区：
文献类型：
--
作者：
Beyersdorff O
最近，Beyersdorff，Bonacina和Chew [10]为量化布尔公式（QBF）引入了一类自然的Frege系统，并证明了这些系统的限制版本的强下界。本文对文献[10]中的新的扩展Frege系统（记作EF + Eschered）进行了全面的分析，它是经典扩展Frege EF的自然扩展，主要结果如下：首先，我们证明了标准的Gentzen式系统G*1 p-模拟EF + Eschered，并且在标准的复杂性理论困难假设下G*1严格更强。我们展示了EF + Bounded算术的对应：EF + Bounded可以被看作是直觉S12的非一致命题版本。具体地说，直觉S12证明的任意语句的前束形式转化为多项式大小的EF +证明，EF +证明是在某种意义上最弱的系统与此属性。最后，我们表明，EF +证明的无条件下界将意味着一个重大突破，无论是在电路的复杂性或在经典的证明复杂性，事实上，匡威的影响，以及持有。因此，系统EF + Eschered自然地团结从电路和证明的复杂性的中心问题。技术上，我们的结果依赖于一个正式的策略提取定理EF + Eschered类似于见证直觉S12和EF + Eschered证明的范式。
Recently Beyersdorff, Bonacina, and Chew [10] introduced a natural class of Frege systems for quantified Boolean formulas (QBF) and showed strong lower bounds for restricted versions of these systems. Here we provide a comprehensive analysis of the new extended Frege system from [10], denoted EF + ∀red, which is a natural extension of classical extended Frege EF.Our main results are the following: Firstly, we prove that the standard Gentzen-style system G*1 p-simulates EF + ∀red and that G*1 is strictly stronger under standard complexity-theoretic hardness assumptions.Secondly, we show a correspondence of EF + ∀red to bounded arithmetic: EF + ∀red can be seen as the non-uniform propositional version of intuitionistic S12. Specifically, intuitionistic S12 proofs of arbitrary statements in prenex form translate to polynomial-size EF + ∀red proofs, and EF + ∀red is in a sense the weakest system with this property.Finally, we show that unconditional lower bounds for EF + ∀red would imply either a major breakthrough in circuit complexity or in classical proof complexity, and in fact the converse implications hold as well. Therefore, the system EF + ∀red naturally unites the central problems from circuit and proof complexity.Technically, our results rest on a formalised strategy extraction theorem for EF + ∀red akin to witnessing in intuitionistic S12 and a normal form for EF + ∀red proofs.
登录
查看更多内容
DOI：
--
发表时间：
1986
期刊：
Symposium on Computation Theory
影响因子：
--
作者：
S. Buss
通讯作者：
S. Buss
DOI：
10.1002/malq.19900360106
发表时间：
1990
期刊：
Math. Log. Q.
影响因子：
--
作者：
J. Krajícek;P. Pudlák
通讯作者：
P. Pudlák
模拟量化命题演算中的非 prenex 削减
影响因子：
0.3
作者：
Emil Jeřábek;Phuong Nguyen
通讯作者：
Phuong Nguyen
关于 QBF 的顺序系统和解析
DOI：
--
发表时间：
2012
期刊：
International Conference on Theory and Applications of Satisfiability Testing
影响因子：
--
作者：
Uwe Egly
通讯作者：
Uwe Egly
影响因子：
0.5
作者：
Beyersdorff, Olaf;Chew, Leroy;Shukla, Anil
通讯作者：
Shukla, Anil