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

若干逻辑自动推理方法研究

作　者: 郭远华
导　师: 曾振柄
学　校: 华东师范大学
专　业: 系统分析与集成
关键词: 定理证明自动推理子句搜索方法一阶逻辑格值逻辑 tableau方法试探方法自然推理方法可读证明
分类号: TP181
类　型: 博士论文
年　份: 2010年
下　载: 197次
引　用: 1次
阅　读: 论文下载

内容摘要

自动定理证明(Automated Theorem Proving)或者机器定理证明(MechanicalTheorem Proving)是通过计算机实现定理证明.二十世纪五十年代以来自动定理证明一直是计算机科学的热点之一,在数学、硬件测试与验证、软件生成与验证、协议验证、人工智能方面都得到了成功的应用.部分实例化方法把一阶问题化为一系列命题逻辑中的可满足性问题来解决一阶逻辑的可满足问题,检查子句集的满足式映射中的阻塞是该方法的关键.论文提出的子句搜索方法在判定子句集可满足性的同时给出了一个模型从而得到满足式映射.格值逻辑的不完全可比性便于描述人类的思维、判断和决策.格值命题逻辑系统LP(X)于1993年建立,目前对LP(X)系统的自动推理研究主要是归结方法,论文讨论了它的tableau方法.常用的逻辑证明方法重点在于判定可满足性而不能给出符合人们阅读习惯的演绎过程.归结方法、语义表方法、相继式方法是定理证明中的常用方法,但是重点在于判定而不是演绎,论文探讨了相干命题逻辑系统R的试探法实现和相干自然推理系统NR的自然推理法实现,生成了类似于手工证明的可读证明.具体而言论文的工作包括以下几方面:(1)提出了子句搜索方法判定命题子句集的可满足性并给出可满足子句集的一个模型.子句搜索方法通过查找到子句集Φ不可扩展的子句C来判定Φ的可满足性.结合部分实例化方法将子句搜索方法提升至一阶,分离了谓词公式的结构和变量,从而提高合一算法的效率并节省了存贮空间.用正整数代表原子,负整数代表负文字,简化了算法实现.(2)提出了格值命题逻辑系统LP(X)的tableau方法,语义表中的公式都是受限蕴涵公式.通过引入Bound~s(X)、Bound_s(X)和极大相容集证明了其正确性和完备性.对于真值域可直积分解的系统LP(X),讨论了其格直积分解证明.(3)提出了后推试探证明方法并将演绎序列中的各公式组织成证明树从而产生了类似于手工证明的演绎序列.将公式转化为二叉树的形式存贮于动态数组中减小了公式冗余,用数组下标代表公式简化了实现.(4)提出了应用于自然推理方法的回溯方法.先从假设集出发构建证明树,再从树根节点逐层推导各公式的属性,实现了相干自然推理系统NR的类似手工证明的自然推理方法证明.综上所述,论文提出了判定子句集可满足性的子句搜索方法并将其提升至一阶,提出了格值命题逻辑系统LP(X)的tableau方法,提出了后推试探方法和回溯方法并实现了相干命题逻辑系统R的可读证明,在理论和应用方面都有积极意义.

全文目录

摘要  6-7
Abstract  7-10
第一章绪论  10-18
  1.1 自动推理的发展简史  10-14
  1.2 非经典逻辑研究概况  14-15
  1.3 论文的选题和主要工作  15-18
第二章一阶子句搜索方法  18-48
  2.1 子句搜索方法  18-24
  2.2 一阶子句搜索方法  24-46
  2.3 本章小结  46-48
第三章格值命题逻辑LP(X)的自动证明  48-68
  3.1 基础知识  48-55
  3.2 LP(X)的tableau方法  55-61
  3.3 LP(X)的直积分解  61-66
  3.4 本章小结  66-68
第四章相干命题逻辑R的可读证明  68-102
  4.1 试探法自动证明  68-80
  4.2 自然推理法自动证明  80-97
  4.3 试探法和自然推理法的混合求证  97-100
  4.4 本章小结  100-102
第五章总结与展望  102-104
参考文献  104-116
致谢  116-117
攻读博士学位期间发表论文和科研情况  117

若干逻辑自动推理方法研究

内容摘要

全文目录

相似论文