• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>AI communications >Implementing a fair monodic temporal logic prover
【24h】

Implementing a fair monodic temporal logic prover

机译：实现公平的单调时间逻辑证明者

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

摘要

Monodic first-order temporal logic is a fragment of first-order temporal logic for which sound and complete calculi have been devised. One such calculus is ordered fine-grained resolution with selection, which is implemented in the theorem prover TeMP. However, the architecture of TeMP cannot guarantee the fairness of its derivations. In this paper we present an architecture for a resolution-based monodic first-order temporal logic prover that can ensure fair derivations and we describe the implementation of this fair architecture in the theorem prover TSPASS.
机译：单调一阶时间逻辑是一阶时间逻辑的一个片段，为此已经设计了声音和完整的演算。一种这样的演算是有选择的有序细粒度解析，在定理证明者TeMP中实现。但是，TeMP的体系结构不能保证其派生的公平性。在本文中，我们提出了一种可确保公平推导的基于分辨率的单调一阶时间逻辑证明器的体系结构，并在定理证明器TSPASS中描述了这种公平体系结构的实现。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号