| 直觉线性μ-演算中的合成推理 |
| |
| 作者姓名： | KAZMISyedAsadRaz 张文辉 |
| |
| 作者单位： | 1. 中国科学院 软件研究所 计算机科学重点实验室,北京 100190;中国科学院 研究生院 信息与工程学院,北京 100049;Department of Computer Science, Government College University, Lahore 54000, Pakistan
2. 中国科学院,软件研究所,计算机科学重点实验室,北京,100190 |
| |
| 基金项目： | Supported by the National Natural Science Foundation of China under Grant Nos.60721061, 60573012 (国家自然科学基金); the National Basic Research Program of China under Grant No.2002CB312200 (国家重点基础研究发展计划(973)) |
| |
| 摘 要： | 讨论了以基于前缀封闭集合的Heyting代数的直觉解释的线性μ-演算(IμTL)作为描述“假设-保证”的逻辑基础的问题,提出了一个基于IμTL的“假设-保证”规则.该规则比往常应用线性时序逻辑(LTL)作为规范语言的那些规则具有更好的表达能力,扩展了对形如“always ?”等安全性质的“假设-保证”的范围,具备更一般的“假设-保证”推理能力及对循环推理的支持.
|
| 关 键 词： | 合成推理 命题线性时序逻辑 直觉线性μ-演算 |
| 收稿时间： | 2008-06-03 |
| 修稿时间： | 2008-08-07 |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
