类型一阶逻辑的理论证明探讨

作     者：徐丹 XU Dan

作者机构：厦门大学计算机科学系福建厦门361005 

出 版 物：《电脑知识与技术》 (Computer Knowledge and Technology)

年 卷 期：2010年第6卷第3期

页      码：1657-1659页

摘      要：类型一阶逻辑在传统的一阶逻辑上,引入了类型,它是多态多类逻辑程序设计语言的理论基础,对编译系统设计与实现的进一步发展具有重要意义。论文在类型一阶逻辑的理论层面进行了探讨,引入了基本简单导出的可靠性定理和等值符号的可替换性定理,并予以证明。通过这两个定理,可以简化类型一阶逻辑理论证明中的工作量,使得将来的理论研究更加方便。

主 题 词：一阶类型逻辑 B类型简单导出 原子简单导出 可靠性 可替换性定理 

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

D　O　I：10.3969/j.issn.1009-3044.2010.07.047

馆 藏 号：203595075...