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

基于扩展规则的定理证明的研究

作　者: 吴瑕
导　师: 孙吉贵
学　校: 吉林大学
专　业: 计算机软件与理论
关键词: 人工智能定理证明自动推理扩展规则化简规则命题逻辑一阶逻辑模态逻辑关系转换破坏性方法函数转换
分类号: TP301
类　型: 博士论文
年　份: 2006年
下　载: 151次
引　用: 4次
阅　读: 论文下载

内容摘要

自动定理证明自从二十世纪五十年代被提出,已经成为计算机科学中最重要的领域之一。归结方法是其中最著名、应用最广的方法之一。扩展规则方法将定理证明沿着归结的反方向进行,是一种新的定理证明方法。为了使扩展规则方法更好的用于定理证明,本文改进和完善了经典逻辑中的扩展规则定理证明方法,提出了模态逻辑中基于扩展规则的定理证明方法。本文的主要贡献如下:(1)用化简规则和启发式对命题扩展规则算法进行改进,从而提高命题扩展规则方法的效率。充分利用基于扩展规则方法和基于归结方法的推理特点来提高推理效率,给出了结合这两种推理方法的结合算法。实验结果表明,我们的改进算法大幅度提高了推理效率,特别是带化简规则和启发式函数的扩展规则算法表现得尤为突出。通过把结合算法与相关工作进行比较,可以看出结合算法是一个快速的命题SAT问题求解器。(2)扩展规则方法是通过部分实例化方法的思想从命题逻辑提升到一阶逻辑的。为了完善Hooker的部分实例化方法,本文重新给出阻塞定义并重新证明了一些定理。为了完善并改进一阶扩展规则算法,本文重新给出潜在阻塞定义,在算法中增加M-可满足的情形,并调用命题逻辑中改进后的扩展规则算法。实现了相应的一阶定理证明器,并用其快速准确的求解了两类非常典型的规划问题。(3)把扩展规则方法推广到模态典逻辑中。通过破坏性方法直接把扩展规则方法推广到模态逻辑中,主要讨论了模态系统K中的破坏性扩展规则方法。实现了相应的模态定理证明器,用其快速的证明了模态系统K中的所有公理和四类标准的benchmark问题。通过关系转换方法和函数转换方法把扩展规则方法推广到模态逻辑中,提出关系扩展规则方法,函数扩展规则方法和广义函数扩展规则方法。

全文目录

第一章绪论  9-30
  1.1 自动推理  9-21
    1.1.1 自动推理的早期历史  9-11
    1.1.2 自动推理的现在  11-12
    1.1.3 自动推理证明方法  12-18
    1.1.4 自动定理证明器  18-19
    1.1.5 自动推理的应用  19-21
  1.2 模态逻辑  21-27
    1.2.1 可能世界语义学  21-22
    1.2.2 结合模态逻辑  22-24
    1.2.3 模态逻辑中的推理方法  24-27
  1.3 本文工作  27-30
第二章改进的命题扩展规则方法  30-48
  2.1 命题扩展规则方法  30-34
    2.1.1 基本命题扩展规则方法ER  30-33
    2.1.2 命题扩展规则方法IER  33-34
  2.2 改进的命题扩展规则方法  34-38
    2.2.1 带化简规则的命题扩展规则方法  34-36
    2.2.2 带化简规则与启发式的命题扩展规则方法  36-38
  2.3 实验结果  38-42
    2.3.1 算法RER、RIER、ER、IER 以及DR 的比较  38-41
    2.3.2 算法IER、RIER 和HRIER 的比较  41-42
  2.4 命题逻辑中扩展规则方法和归结方法的结合  42-47
  2.5 小结  47-48
第三章一阶扩展规则方法  48-66
  3.1 基础知识  48-49
  3.2 一阶逻辑中部分实例化推理方法  49-56
    3.2.1 部分实例化和阻塞  49-53
    3.2.2 部分实例化方法  53-56
  3.3 一阶逻辑中扩展规则方法及其实现  56-64
    3.3.1 一阶扩展规则方法  56-59
    3.3.2 一阶扩展规则方法证明器  59-64
  3.4 小结  64-66
第四章关系扩展规则方法和破坏性扩展规则方法  66-87
  4.1 模态逻辑  66-70
    4.1.1 语法  66-68
    4.1.2 语义  68-70
  4.2 关系扩展规则  70-74
    4.2.1 关系转换  70-71
    4.2.2 关系扩展规则方法  71-73
    4.2.3 讨论  73-74
  4.3 破坏性扩展规则  74-86
    4.3.1 非子句形式的扩展规则方法  75-78
    4.3.2 命题模态逻辑K 中的推理  78-83
    4.3.3 其它命题模态逻辑中的推理  83-84
    4.3.4 实验结果  84-86
  4.4 小结  86-87
第五章函数扩展规则方法  87-108
  5.1 函数转换  87-98
    5.1.1 函数语义  87-91
    5.1.2 对应理论  91-94
    5.1.3 函数转换  94-98
  5.2 路径与语法合一  98-103
    5.2.1 路径和前缀稳定  98-100
    5.2.2 语法合一  100-103
  5.3 函数转换扩展规则方法  103-107
    5.3.1 连续函数扩展规则方法  103-105
    5.3.2 一般函数扩展规则方法  105-107
  5.4 小结  107-108
第六章总结与展望  108-111
参考文献  111-121
作者读博士期间完成的论文与参加的科研项目  121-123
致谢  123-124
摘要  124-128
ABSTRACT  128-132

基于扩展规则的定理证明的研究

内容摘要

全文目录

相似论文