• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Computer Science Logic >Resolution Refutations and Propositional Proofs with Height-Restrictions
【24h】

Resolution Refutations and Propositional Proofs with Height-Restrictions

机译：具有高度限制的分辨率反驳和命题证明

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

摘要

Height restricted resolution (proofs or refutations) is a natural restriction of resolution where the height of the corresponding proof tree is bounded. Height restricted resolution does not distinguish between tree- and sequence-like proofs. We show that polylogarithmic-height resolution is strongly connected to the bounded arithmetic theory S(1/2)(α). We separate polylogarithmic-height resolution from quasi-polynomial size tree-like resolution. Inspired by this we will study infinitely many sub-linear-height restrictions given by functions n n → 2_i ((log~(i+1)_n)~(O(1)) for i ≥ 0. We show that the resulting resolution systems are connected to certain bounded arithmetic theories, and that they form a strict hierarchy of resolution proof systems. To this end we will develop some proof theory for height restricted proofs.
机译：高度限制的分辨率（证明或反驳）是对分辨率的自然限制，其中相应的证明树的高度是有界的。高度受限的分辨率无法区分树状证明和序列状证明。我们表明，多对数高度分辨率与有界算术理论S（1/2）（α）密切相关。我们将多对数高度分辨率与拟多项式大小树形分辨率分开。受此启发，我们将无限研究函数nn→2_i（（log〜（i + 1）_n）〜（O（1））对于i≥0给出的许多子线性高度限制。我们证明了所得的分辨率系统与某些有界算术理论联系在一起，它们形成了严格的分辨率证明系统层次结构，为此，我们将为高度受限证明开发一些证明理论。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号