Frege Systems for Quantified Boolean Logic
Frege Systems for Quantified Boolean Logic
复制标题
DOI：
10.1145/3381881
复制
发表时间：
2020-05-01
影响因子：
2.5
通讯作者：
Pich, Jan
中科院分区：
文献类型：
--
作者：
Beyersdorff, Olaf;Bonacina, Ilario;Pich, Jan
我们定义和研究Frege系统的量化布尔公式（QBF）。对于这些新的证明系统，我们开发了一个下界技术，直接升降机电路C类的电路下限的QBF弗雷格系统从C线操作。这种从电路到证明复杂性下界的直接转换经常被假设用于命题系统，但在此之前还没有正式建立任何证明系统的这种普遍性。这导致了QBF Frege的限制版本的强下界，特别是与AC（0）[p]电路一起运行的QBF Frege系统的指数下界。相比之下，AC（0）[p]-Frege命题的任何非平凡下界都是一个主要的公开问题，而将这些下界改进为无限制的QBF Frege则紧密对应于电路复杂性和命题证明复杂性的主要问题。特别地，证明了任意P/poly电路的QBF Frege系统的下界等价于证明了P/poly电路或命题扩展Frege（P/poly电路）的下界.我们还将我们的新QBF Frege系统与QBF的标准微积分进行了比较，并建立了与直觉有界算术的对应关系.
We define and investigate Frege systems for quantified Boolean formulas (QBF). For these new proof systems, we develop a lower bound technique that directly lifts circuit lower bounds for a circuit class C to the QBF Frege system operating with lines from C. Such a direct transfer from circuit to proof complexity lower bounds has often been postulated for propositional systems but had not been formally established in such generality for any proof systems prior to this work.This leads to strong lower bounds for restricted versions of QBF Frege, in particular an exponential lower bound for QBF Frege systems operating with AC(0)[p] circuits. In contrast, any non-trivial lower bound for propositional AC(0)[p]-Frege constitutes a major open problem.Improving these lower bounds to unrestricted QBF Frege tightly corresponds to the major problems in circuit complexity and propositional proof complexity. In particular, proving a lower bound for QBF Frege systems operating with arbitrary P/poly circuits is equivalent to either showing a lower bound for P/poly or for propositional extended Frege (which operates with P/poly circuits).We also compare our new QBF Frege systems to standard sequent calculi for QBF and establish a correspondence to intuitionistic bounded arithmetic.