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

1、yiT论女第表超凉若干逻辑自动推理方法研究【摘要】：自动定理证明(AutomatedTheoremProving咸者机器定理证 明(Mecha nicalTheoremProvi ng)是通过计算机实现定理证明.二十世纪 五十年代以来自动定理证明一直是计算机科学的热点之一，在数学、硬件测试与验证、软件生成与验证、协议验证、人工智能方面都得到 了成功的应用部分实例化方法把一阶问题化为一系列命题逻辑中的 可满足性问题来解决一阶逻辑的可满足问题，检查子句集的满足式映射中的阻塞是该方法的关键论文提出的子句搜索方法在判定子句集 可满足性的同时给出了一个模型从而得到满足式映射格值逻辑的不完全可比性便于描述

2、人类的思维、判断和决策.格值命题逻辑系统LP(X)于1993年建立，目前对LP(X)系统的自动推理研究主要是归结 方法，论文讨论了它的tableau方法.常用的逻辑证明方法重点在于判定 可满足性而不能给出符合人们阅读习惯的演绎过程归结方法、语义表方法、相继式方法是定理证明中的常用方法，但是重点在于判定而不是演绎，论文探讨了相干命题逻辑系统R的试探法实现和相干自然推理系统NR的自然推理法实现，生成了类似于手工证明的可读证明 具体而言论文的工作包括以下几方面:(1)提出了子句搜索方法判定命 题子句集的可满足性并给出可满足子句集的一个模型子句搜索方法通过查找到子句集不可扩展的子句C来判定的可满足性结

3、合部 分实例化方法将子句搜索方法提升至一阶，分离了谓词公式的结构和 变量，从而提高合一算法的效率并节省了存贮空间用正整数代表原子负整数代表负文字，简化了算法实现.(2)提出了格值命题逻辑系统 LP(X)的tableau方法,语义表中的公式都是受限蕴涵公式通过引入Bounds(X)、Bound_s(X)和极大相容集证明了其正确性和完备性.对 于真值域可直积分解的系统 LP(X),讨论了其格直积分解证明.(3)提出 了后推试探证明方法并将演绎序列中的各公式组织成证明树从而产 生了类似于手工证明的演绎序列将公式转化为二叉树的形式存贮于 动态数组中减小了公式冗余，用数组下标代表公式简化了实现.(4)提

4、 出了应用于自然推理方法的回溯方法先从假设集出发构建证明树，再 从树根节点逐层推导各公式的属性，实现了相干自然推理系统 NR的 类似手工证明的自然推理方法证明综上所述，论文提出了判定子句集 可满足性的子句搜索方法并将其提升至一阶，提出了格值命题逻辑系 统LP(X)的tableau方法,提出了后推试探方法和回溯方法并实现了相 干命题逻辑系统R的可读证明，在理论和应用方面都有积极意义.【关 键词】：定理证明自动推理子句搜索方法一阶逻辑格值逻辑tableau方法试探方法自然推理方法可读证明【学位授予单位】：华东师范大学【学位级别】：博士【学位授予年份】：2010【分类号】：TP181yiT 论女第表

5、&彖【目录】：摘要6-7Abstract7-10第一章绪论10-181.1自动推理的发展 简史10-141.2非经典逻辑研究概况14-151.3论文的选题和主要工作15-18第二章一阶子句搜索方法18-482.1子句搜索方法18-242.2 一阶 子句搜索方法24-462.3本章小结46-48第三章格值命题逻辑LP(X)的 自动证明 48-683.1基础知识 48-553.2LP(X)的tableau方法 55-613.3LP(X)的直积分解61-663.4本章小结66-68第四章相干命题逻 辑R的可读证明68-1024.1试探法自动证明68-804.2自然推理法自动 证明80-974.3试探法和自然推理法的混合求证 97-1004.4本章小结