首页> 中文期刊> 《上海大学学报：自然科学版》 >一个定理证明检查器

一个定理证明检查器

开具论文收录证明 >>

期刊封面封底目录下载 >>

文献代查 >>

页面导航

摘要
著录项
相似文献
相关主题

摘要

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

著录项

来源
《上海大学学报：自然科学版》 |2000年第1期|63-66|共4页
作者
顾永立; 顾训穰; 谢步罡;
展开▼
作者单位

复旦大学管理学院;

上海大学计算机学院;

上海电视大学;

展开▼
原文格式 PDF
正文语种 chi
中图分类证明论;人工智能理论;
关键词
类型检查; 定理证明; 归约; 重命名; 演算; 检查器;

相似文献

中文文献
外文文献
专利

1. 使用TestMX测试远程电子邮件服务器的连接性——使用一个简单命令轻松检查连接性 [J] . . Windows IT Pro Magazine：国际中文版 . 2009,第002期
2. 一个经过证明的类型化汇编语言的类型检查器 [J] . 郭宇 ,陈意云 ,华保健 . 小型微型计算机系统 . 2008,第007期
3. 检查空气滤清器滤清效果的一个方法 [J] . 王惠盛 . 农业机械 . 2007,第04B期
4. 一个前摄性口令检查器的设计 [J] . 李频 . 计算机应用与软件 . 2004,第009期
5. 检查节温器的一个简便方法 [J] . 曲传晓 . 山东农机化 . 2000,第003期
6. 关于Hale的《常微分方程》一书中一个定理证明的注记 [C] . 张无畏 . 第二届全国青年常微分方程理论与应用学术会议 . 1998
7. 一个用于手机收发器的数模转换器电路设计 [A] . 沈剑 . 2008

获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

客服微信
服务号