一个定理证明检查器

作     者：顾永立 顾训穰 谢步罡 GU Yong- li1, GU Xun- rang2 , XIE Bu- gang3 ( 1.Fudan U niversity,Shanghai 2 0 0 4 3 3 ,China;2 .Shanghai U niversity,Shanghai 2 0 0 0 72 ,China;3 .Shanghai TV University,Shanghai 2 0 180 0 ,China)

作者机构：复旦大学管理学院上海200433 上海大学计算机学院上海200072 上海电视大学上海201800 

出 版 物：《上海大学学报（自然科学版）》 (Journal of Shanghai University:Natural Science Edition)

年 卷 期：2000年第6卷第1期

页      码：63-66页

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

主 题 词：类型检查 定理证明 归约 重命名 演算 检查器 

学科分类：01[哲学] 12[管理学] 07[理学] 08[工学] 070104[070104] 0101[哲学-哲学类] 1201[管理学-管理科学与工程类] 010104[010104] 081104[081104] 0835[0835] 0701[理学-数学类] 0811[工学-水利类] 0812[工学-测绘类] 

D　O　I：10.3969/j.issn.1007-2861.2000.01.015

馆 藏 号：203572627...