| 面向时序逻辑的证明系统：INCAPS |
| 何锫
|
| 1989
|
| 学位授予单位 | 中国科学院软件研究所
|
| 学位 | 博士
|
| 学位授予地点 | 中国科学院软件研究所
|
| 摘要 | INCAPS是一个面向时序逻辑的计算机辅助证明系统，本文主要讨论其中四个问题：INCAPS的向后推理机制——tactics及tacticals；以例子说明用INCAPS进行程序正确性证明的具体实施过程；利用INCAPS的推理机制验证AB协议的层次说明；INCAPS与LCF的异同比较。关于向后推理机制的讨论是本文论述的重点。在这里，除详尽介绍了tactics和tacticals的类别及结构以外，还围绕（复合）tactics的有效性问题，通过引入（复合）tactics的层次数，函数树及树上的B函数等概念作了进一步的探讨。我们的结论是：INCAPS系统中（复合）tactics是有效的。 |
| 语种 | 中文
|
| 内容类型 | 学位论文
|
| URI标识 | http://ir.iscas.ac.cn/handle/311060/6754
|
| 专题 | 中科院软件所_中科院软件所
|
推荐引用方式
GB/T 7714 |
何锫. 面向时序逻辑的证明系统：INCAPS[D]. 中国科学院软件研究所. 中国科学院软件研究所,1989.
|
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论