一个定理证明检查器

摘要：

介绍了一种新型的形式说明语言PD_Cal,该语言具有良好的表达能力以及丰富的类型.通过对由该语言描述的定理证明过程进行类型检查,可判断该证明是否是给定定理的正确的证明.在该思想的基础上,设计并实现了PD-Cal定理证明检查器.

关键词：类型检查、定理证明、归约、重命名

所属期刊栏目：6

分类号：TP18(自动化基础理论)

在线出版日期：2004-01-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：63-66