定理证明辅助工具Isabelle剖析与应用  

ANALYSIS AND APPLICATION OF THEOREM-PROVING AIDING TOOLS——ISABELLE

作　　者：郭慧梅[1] 缪淮扣[1] 陈怡海[1] 

机构地区：[1]上海大学计算机工程与科学学院,上海200072

出　　处：《计算机应用与软件》2007年第8期14-16,43,共4页Computer Applications and Software

基　　金：国家自然科学基金项目(60373072;60673115);上海市教委科技发展基金(05AZ70)。

摘　　要：Isabelle是一个通用的定理证明器,应用领域广泛。介绍Isabelle逻辑系统的功能和构成,分析了Isabelle的规格说明语言、验证系统的特点,并给出了用Isabelle逻辑系统来构造Z规格说明的定理证明的方法。Isabelle is a genetic theorem proving environment. Its application area is broad. The function and structure of Isabelle are introduced,and the features of Isabelle＇s logic system are analyzed. The method to construct theorem proving of Z specification by using Isabelle＇s logic system is given.

关 键 词：逻辑系统 定理证明器 形式化方法 

分 类 号：TP301.1[自动化与计算机技术—计算机系统结构]