区间逻辑的一个辅助证明工具

摘要：

DC/P(duration calculus prover)是一族实时区间逻辑的辅助定理证明工具.它采用Gentzen风格相继式演算作为基本证明系统,并结合项重写、自动判定算法等技术以提高证明的自动化程序.该文介绍了DC/P的语义编码方法、采用的相继式证明系统及实现技术,并给出了应用实例.

关键词：邻域逻辑、区间时序逻辑、均值演算、时段演算、相继式演算、定理证明

所属期刊栏目：11

分类号：TP301(计算技术、计算机技术)

资助基金：中国科学院资助项目69873045;高比容电子铝箔的研究开发与应用项目863-306-ZT06-04-1;UNU/IISTInternational Institute for Software Technology, United Nations University项目

在线出版日期：2004-01-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：116-121