首页> 外文期刊>IEICE Transactions on Information and Systems >Strong Contraction in Model Elimination Calculus: Implementation in a PTTP-Based Theorem Prover
【24h】

Strong Contraction in Model Elimination Calculus: Implementation in a PTTP-Based Theorem Prover

机译:模型消除演算中的强收缩:在基于PTTP的定理证明中的实现

获取原文
获取原文并翻译 | 示例
       

摘要

In this paper, we propose a new lemma facility, called the strong contraction rule, for model elimination calculus, and we study some implementation issues of strong contraction in a PTTP-based theorem prover. Strong contraction has the ability to shorten possible proofs and prevent some irrelevant computation to a target goal. Strong contraction never broadens the search space, in principle, and thus, has a stable effect on the acceleration of top-down proof search. However, it is diffi- cult to embed the strong contraction into a PTTP-based theorem prover, because strong contraction imposes a truncation opera- tion of center chains in model elimination calculus.
机译:在本文中,我们为模型消除演算提出了一种新的引理工具,称为强收缩规则,并在基于PTTP的定理证明者中研究了强收缩的一些实现问题。强收缩具有缩短可能的证明并防止与目标目标无关的某些计算的能力。原则上,强收缩永远不会扩大搜索空间,因此,对加速自顶向下证明搜索具有稳定的作用。但是,很难将强压缩嵌入到基于PTTP的定理证明中,因为强压缩在模型消除演算中强加了中心链的截断操作。

著录项

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号