证明策略及其有效性问题
DOI:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

国家自然科学基金


PROOF STRATEGIES AND VALIDITY
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    INCAPS(INteractiv Computer-Aided Proving System)是一个面向时序逻辑的交互式计算机辅助证明系统。本文简要介绍了其证明策略(tactics,tacticals)的类别、结构,并在引入证明策略的层次数、函数树及树上B函数等新概念前提下,深入探讨和证明了IN-CAPS证明策略的有效性问题。

    Abstract:

    INCAPS (INteractive Computer-Aided Proving System) is a proof system of temporal logic. This paper outlines its proof strategies (tactics, tacticals) variety and structure. The kernel of it is to discuss the validity of tactics and tacticals. After introducing several new concepts: proof strategies level number, function tree and B function defined on it, we show that INCAPS proof strategies are valid.

    参考文献
    相似文献
    引证文献
引用本文

何锫.证明策略及其有效性问题.软件学报,1991,2(4):23-30

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:1989-11-24
  • 最后修改日期:1990-03-26
  • 录用日期:
  • 在线发布日期:
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号