• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>AI communications >CTL-RP: A computation tree logic resolution prover
【24h】

CTL-RP: A computation tree logic resolution prover

机译：CTL-RP：计算树逻辑分辨率证明器

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

摘要

In this paper, we present a resolution-based calculus R_(CTL)~(γ,S) for Computation Tree Logic (CTL) as well as an implementation of that calculus in the theorem prover CTL-RP. The calculus R_(CTL)~(γ,S) requires a transformation of an arbitrary CTL formula to an equi-satisfiable clausal normal form formulated in an extension of CTL with indexed path formulae. The calculus itself consists of a set of resolution rules which can be used for an EXPTIME decision procedure for the satisfiability problem of CTL. We give a formal semantics for the clausal normal form, provide proof sketches for the soundness and completeness of the resolution rules, discuss the complexity of the decision procedure based on R_(CTL)~(γ,S), and present an approach to implementing the calculus R_(CTL)~(γ,S) first-order techniques. Finally, we give a comparison between CTL-RP and a tableau theorem prover forrnCTL.
机译：在本文中，我们为计算树逻辑（CTL）提出了基于分辨率的演算R_（CTL）〜（γ，S）以及该演算在定理证明者CTL-RP中的实现。演算R_（CTL）〜（γ，S）需要将任意CTL公式转换为等价的常规正态形式，该形式由带有索引路径公式的CTL扩展形成。演算本身包含一组解析规则，这些规则可用于CTL可满足性问题的EXPTIME决策过程。我们给出了子句范式的形式语义，为解析规则的健全性和完整性提供了证明草图，讨论了基于R_（CTL）〜（γ，S）的决策过程的复杂性，并提出了一种实现方法微积分R_（CTL）〜（γ，S）一阶技术。最后，我们对CTL-RP和forrnCTL的一个定理证明者进行了比较。

著录项

  • 来源
    《AI communications》 |2010年第3期|p.111-136|共26页
  • 作者

    Lan Zhang; Ullrich Hustadt; Clare Dixon;

  • 作者单位

    Department of Computer Science, University of Liverpool, Liverpool, UK;

    rnDepartment of Computer Science, University of Liverpool, Liverpool, UK;

    rnDepartment of Computer Science, University of Liverpool, Liverpool, UK;

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

    branching-time temporal logics; resolution theorem proving;

    机译：分支时间时序逻辑;分辨率定理证明;

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号