学位论文 > 优秀研究生学位论文题录展示

Isabelle中自动化证明策略的设计与实现

作　者: 程应娥
导　师: 李廉
学　校: 兰州大学
专　业: 计算机软件与理论
关键词: 定理机器证明 Isabelle 策略
分类号: TP311.52
类　型: 硕士论文
年　份: 2007年
下　载: 58次
引　用: 2次
阅　读: 论文下载

内容摘要

定理机器证明是人工智能的一个重要研究领域，被应用在数学定理证明、协议验证、软件和硬件的形式化验证等方面。提高定理机器证明的效率仍然受到人工智能界的重视。人们开发了各种定理证明系统，主要有自动化和交互式两种类型。Isabelle/Isay/HOL(以下简称Isabelle)是基于高阶逻辑的交互式定理证明器，它是由英国剑桥大学的Lawrence C.Paulson教授和德国慕尼黑技术大学的Tobias Nipkow教授于1986年开始联合开发的，并在不断的更新和发展。在Isabelle中定理证明的主要方法是策略，证明过程是由用户提交策略，再由机器执行策略的交互过程。本文在分析了Isabelle最基本的证明策略的基础上，通过在Isabelle集成环境中添加控制模块(Ctrl Block)，完成了一种并行自动化证明策略的系统设计。该控制模块负责解释并执行并行策略，完成各进程间的通信。该系统的运行环境为支持MPI编程标准的并行计算机或微机机群，由多个协同完成证明任务的Isabelle进程组成，采用主从模式的大粒度并行算法。主进程位于用户计算机中，从进程位于选定的机群中。主进程负责控制整个并行程序，分配证明任务给从进程，等待从进程报告证明的结果，再根据结果判断证明是完成还是失败。从进程等待主进程给它分配证明任务，接到并完成任务后向主进程报告证明的结果，然后继续等待主进程分配的任务或停止指令。

全文目录

摘要  4-5
Abstract  5-6
目录  6-7
第一章绪论  7-9
  1.1 论文的研究背景  7-8
  1.2 问题的提出  8
  1.3 主要工作  8
  1.4 论文提纲  8-9
第二章定理机器证明简介  9-14
  2.1 定理机器证明  9
  2.2 定理机器证明的研究概况  9-13
  2.3 定理证明器的分类  13-14
第三章 Isabelle简介  14-31
  3.1 Isabelle系统结构  14-20
    3.1.1 ML语言  15-17
    3.1.2 Isabelle的逻辑  17-18
    3.1.3 提升规则(lifting rule)  18-20
  3.2 Isabelle定理证明方法  20-23
  3.3 Isabelle证明理论  23-25
  3.4 Isabelle的策略和策略算子  25-31
第四章自动化证明策略的设计和实现  31-54
  4.1 系统结构  31-43
  4.2 用户接口  43-46
  4.3 算法设计  46-54
第五章总结与展望  54-58
致谢  58

Isabelle中自动化证明策略的设计与实现

内容摘要

全文目录

相似论文