• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Annual ACM/IEEE Symposium on Logic in Computer Science >From positive and intuitionistic bounded arithmetic to monotone proof complexity
【24h】

From positive and intuitionistic bounded arithmetic to monotone proof complexity

机译：从正直觉有界算术到单调证明复杂性

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

摘要

We study versions of second-order bounded arithmetic where induction and comprehension formulae are positive or where the underlying logic is intuitionistic, examining their relationships to monotone and deep inference proof systems for propositional logic. In the positive setting a restriction of a Paris-Wilkie (PW) style translation yields quasipolynomial-size monotone propositional proofs from Π10 arithmetic theorems, as expected. We further show that, when only polynomial induction is used, quasipolynomialsize normal deep inference proofs may be obtained, via a graph-rewriting normalisation procedure from earlier work. For the intuitionistic setting we calibrate the PW translation with the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic implication to recover a transformation to monotone proofs. By restricting type level we are able to identify an intuitionistic theory, I1U21, for which the transformation yields quasipolynomialsize monotone proofs. Conversely, we show that I1U21 is powerful enough to prove the soundness of monotone proofs, thereby establishing a full correspondence.
机译：我们研究了二阶有界算术的版本，在这些版本中，归纳和理解公式为正，或者底层逻辑是直觉的，检查了它们与命题逻辑的单调和深层推理证明系统的关系。在肯定的情况下，对巴黎-威尔基（PW）风格的限制会产生从Π到拟多项式大小的单调命题证明 1 0 如预期的算术定理。我们进一步表明，当仅使用多项式归纳法时，可以通过早期工作中的图形重写归一化程序来获得准多项式大小的正常深度推断证明。对于直觉设置，我们使用直觉暗示的Brouwer-Heyting-Kolmogorov解释来校准PW翻译，以恢复对单调证明的转换。通过限制类型级别，我们可以确定一种直觉理论， 1 ü 2 1 ，为此变换可生成拟多项式大小的单调证明。相反，我们表明我 1 ü 2 1 足够强大，足以证明单调证明的可靠性，从而建立完整的对应关系。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号