|
|||||
|
|
| 定理证明辅助工具Isabelle剖析与应用 | |
| 引用本文： | 郭慧梅,缪淮扣,陈怡海.定理证明辅助工具Isabelle剖析与应用[J].计算机应用与软件,2007,24(8):14-16,43. |
| 作者姓名： | 郭慧梅 缪淮扣 陈怡海 |
| 作者单位： | 上海大学计算机工程与科学学院,上海,200072;上海大学计算机工程与科学学院,上海,200072;上海大学计算机工程与科学学院,上海,200072 |
| 基金项目： | 国家自然科学基金 , 上海市教委资助项目 |
| 摘 要： | Isabelle是一个通用的定理证明器,应用领域广泛.介绍Isabelle逻辑系统的功能和构成,分析了Isabelle的规格说明语言、验证系统的特点,并给出了用Isabelle逻辑系统来构造Z规格说明的定理证明的方法. |
| 关 键 词： | 逻辑系统 定理证明器 形式化方法 |
| 修稿时间： | 2005-08-22 |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ | |