Institutional Repository
| 面向时序逻辑的证明系统：INCAPS | |
| 何锫 | |
| 1989 | |
| Degree Grantor | 中国科学院软件研究所 |
| Degree Level | 博士 |
| Place of Degree Grantor | 中国科学院软件研究所 |
| English Abstract | INCAPS是一个面向时序逻辑的计算机辅助证明系统，本文主要讨论其中四个问题：INCAPS的向后推理机制——tactics及tacticals；以例子说明用INCAPS进行程序正确性证明的具体实施过程；利用INCAPS的推理机制验证AB协议的层次说明；INCAPS与LCF的异同比较。关于向后推理机制的讨论是本文论述的重点。在这里，除详尽介绍了tactics和tacticals的类别及结构以外，还围绕（复合）tactics的有效性问题，通过引入（复合）tactics的层次数，函数树及树上的B函数等概念作了进一步的探讨。我们的结论是：INCAPS系统中（复合）tactics是有效的。 |
| Language | 中文 |
| Content Type | 学位论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/6754 |
| Collection | 中科院软件所_中科院软件所 |
| Recommended Citation GB/T 7714 | 何锫. 面向时序逻辑的证明系统：INCAPS[D]. 中国科学院软件研究所. 中国科学院软件研究所,1989. |
| Files in This Item: | ||||||
| File Name/Size | DocType | Version | Access | License | ||
| N84458.pdf（1455KB） | 限制开放 | -- | Application Full Text | |||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment