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

论文摘要

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

论文目录

• 第一章 绪论
• 1.1 自动推理
• 1.1.1 自动推理的早期历史
• 1.1.2 自动推理的现在
• 1.1.3 自动推理证明方法
• 1.1.4 自动定理证明器
• 1.1.5 自动推理的应用
• 1.2 模态逻辑
• 1.2.1 可能世界语义学
• 1.2.2 结合模态逻辑
• 1.2.3 模态逻辑中的推理方法
• 1.3 本文工作
• 第二章 改进的命题扩展规则方法
• 2.1 命题扩展规则方法
• 2.1.1 基本命题扩展规则方法ER
• 2.1.2 命题扩展规则方法IER
• 2.2 改进的命题扩展规则方法
• 2.2.1 带化简规则的命题扩展规则方法
• 2.2.2 带化简规则与启发式的命题扩展规则方法
• 2.3 实验结果
• 2.3.1 算法RER、RIER、ER、IER 以及DR 的比较
• 2.3.2 算法IER、RIER 和HRIER 的比较
• 2.4 命题逻辑中扩展规则方法和归结方法的结合
• 2.5 小结
• 第三章 一阶扩展规则方法
• 3.1 基础知识
• 3.2 一阶逻辑中部分实例化推理方法
• 3.2.1 部分实例化和阻塞
• 3.2.2 部分实例化方法
• 3.3 一阶逻辑中扩展规则方法及其实现
• 3.3.1 一阶扩展规则方法
• 3.3.2 一阶扩展规则方法证明器
• 3.4 小结
• 第四章 关系扩展规则方法和破坏性扩展规则方法
• 4.1 模态逻辑
• 4.1.1 语法
• 4.1.2 语义
• 4.2 关系扩展规则
• 4.2.1 关系转换
• 4.2.2 关系扩展规则方法
• 4.2.3 讨论
• 4.3 破坏性扩展规则
• 4.3.1 非子句形式的扩展规则方法
• 4.3.2 命题模态逻辑K 中的推理
• 4.3.3 其它命题模态逻辑中的推理
• 4.3.4 实验结果
• 4.4 小结
• 第五章 函数扩展规则方法
• 5.1 函数转换
• 5.1.1 函数语义
• 5.1.2 对应理论
• 5.1.3 函数转换
• 5.2 路径与语法合一
• 5.2.1 路径和前缀稳定
• 5.2.2 语法合一
• 5.3 函数转换扩展规则方法
• 5.3.1 连续函数扩展规则方法
• 5.3.2 一般函数扩展规则方法
• 5.4 小结
• 第六章 总结与展望
• 参考文献
• 作者读博士期间完成的论文与参加的科研项目
• 致谢
• 摘要
• ABSTRACT