|
|||||
|
|
| 一个定理证明检查器 | |
| 引用本文： | 顾永立,顾训穰,谢步罡. 一个定理证明检查器[J]. 上海大学学报(自然科学版), 2000, 6(1): 63-66 |
| 作者姓名： | 顾永立 顾训穰 谢步罡 |
| 作者单位： | 1. 复旦大学,管理学院,上海,200433 2. 上海大学,计算机学院,上海,200072 3. 上海电视大学,上海,201800 |
| 摘 要： | 介绍了一种新型的形式说明语言ＰＤ－Ｃａｌ，该语言具有良好的表达能力以及丰富的类型。通过对由该语言描述的定理证明过程进行类型检查，可判断该证明是否是给定定理的正确的证明。在该思想的基础上，设计并实现了ＰＤ－Ｃａｌ定理证明检查器。 |
| 关 键 词： | 类型检查 定理证明 归约 重命名 演算 检查器 |
A Theorem Proof Checker |
|
| GU Yong- li,GU Xun- rang,XIE Bu- gang. A Theorem Proof Checker[J]. Journal of Shanghai University(Natural Science), 2000, 6(1): 63-66 | |
| Authors: | GU Yong- li GU Xun- rang XIE Bu- gang |
| Affiliation: | GU Yong- li1,GU Xun- rang2,XIE Bu- gang3 |
| Abstract: | |
| Keywords: | type check theorem proof reduce rename |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ | |