• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>AI communications >TPTP, CASC and the development of a semantically guided theorem prover
【24h】

TPTP, CASC and the development of a semantically guided theorem prover

机译：TPTP，CASC和语义指导定理证明者的发展

获取原文
获取原文并翻译 | 示例
       
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

The first-order theorem prover SCOTT has been through a series of versions over some ten years. The successive provers, while retaining the same underlying technology, have used radically different algorithms and shown wide differences of behaviour. The development process has depended heavily on experiments with problems from the TPTP library and has been sharpened by participation in CASC each year since 1997. In the present paper, we outline some of the difficulties inherent in designing and refining a theorem prover as complex as SCOTT, and explain our experimental methodology. While SCOTT is not one of the systems which have been highly optimised for CASC, it does help to illustrate the influence of both CASC and the TPTP library on contemporary theorem proving research.
机译：一阶定理证明者SCOTT已经经历了十多年的一系列版本。后续证明，在保留相同基础技术的同时，使用了根本不同的算法，并表现出很大的差异。开发过程在很大程度上依赖于TPTP库中存在问题的实验，并且自1997年以来每年都因参加CASC而变得更加敏锐。在本文中，我们概述了设计和完善定理证明者（如SCOTT）所固有的一些困难。 ，并说明我们的实验方法。尽管SCOTT并不是针对CASC进行了高度优化的系统之一，但它确实有助于说明CASC和TPTP库对当代定理证明研究的影响。

著录项

  • 来源
    《AI communications》 |2002年第3期|p.135-146|共12页
  • 作者

    Kahlil Hodgson; John Slaney;

  • 作者单位

    Computer Sciences Laboratory, RSISE, The Australian National University, Canberra, ACT 0200, Australia;

  • 收录信息 美国《科学引文索引》(SCI);美国《工程索引》(EI);
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类 人工智能理论;
  • 关键词

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号