摘要
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.
出处
《计算机应用与软件》
CSCD
北大核心
2007年第8期14-16,43,共4页
Computer Applications and Software
基金
国家自然科学基金项目(60373072
60673115)
上海市教委科技发展基金(05AZ70)。
