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

• 作者: 王戟 胡成军 陈火旺
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 邻域逻辑 区间时序逻辑 均值演算 时段演算 相继式演算 定理证明
• 年，卷（期）: 2000,（1）
• 页码范围: 116-121
• 页数: 6页
• 分类号: TP301
• 字数: 4673字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈火旺	国防科学技术大学计算机学院	53	2116	23.0	45.0
2	王戟	国防科学技术大学计算机学院	44	1257	17.0	35.0
3	胡成军	国防科学技术大学计算机学院	5	41	3.0	5.0