• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Annual ACM/IEEE Symposium on Logic in Computer Science >Understanding Gentzen and Frege Systems for QBF
【24h】

Understanding Gentzen and Frege Systems for QBF

机译：了解QBF的Gentzen和Frege系统

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

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 EE + Vred, which is a natural extension of classical extended Frege EE. Our main results are the following: Firstly, we prove that the standard Gentzen-style system G*1 p-simulates EE + Vred and that G*1 is strictly stronger under standard complexity-theoretic hardness assumptions. Secondly, we show a correspondence of EE + Vred to bounded arithmetic: EE + Vred 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 EE + Vred proofs, and EE + Vred is in a sense the weakest system with this property. Finally, we show that unconditional lower bounds for EE + Vred 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 EE + Vred naturally unites the central problems from circuit and proof complexity. Technically, our results rest on a formalised strategy extraction theorem for EE + Vred akin to witnessing in intuitionistic S12 and a normal form for EE + Vred proofs.
机译：最近，Beyersdorff，Bonacina和Chew [10]为量化布尔公式（QBF）引入了自然类的Frege系统，并显示了这些系统的受限版本的强下界。在这里，我们提供了对[10]中新扩展的Frege系统的全面分析，表示为EE + Vred，这是对经典扩展Frege EE的自然扩展。我们的主要结果如下：首先，我们证明标准的Gentzen样式系统G * 1 p模拟EE + Vred和G * 1 在标准复杂度-理论硬度假设下，严格更强。其次，我们展示EE + Vred与有界算术的对应关系：EE + Vred可看作是直觉S12的非一致命题版本。具体来说，先验形式的任意语句的直觉S12证明会转换为多项式大小EE + Vred证明，并且EE + Vred在某种意义上是具有此属性的最弱系统。最后，我们表明EE + Vred的无条件下界将意味着电路复杂性或经典证明复杂性的重大突破，实际上，相反的含义也成立。因此，系统EE + Vred自然地将电路和证明复杂性方面的核心问题结合在一起。从技术上讲，我们的结果基于EE + Vred的形式化策略提取定理，类似于直观的S12中的见证和EE + Vred证明的正常形式。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号