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

《若干逻辑自动推理方法研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、华东师范大学博士学位论文若干逻辑自动推理方法研究姓名：郭远华申请学位级别：博士专业：系统分析与集成指导教师：曾振柄20091001摘要自动定理证明(AutomatedTheoremProving)或者机器定理证明(MechanicalTheoremProving)是通过计算机实现定理证明．二十世纪五十年代以来自动定理证明一直是计算机科学的热点之一，在数学、硬件测试与验证、软件生成与验证、协议验证、人工智能方面都得到了成功的应用．部分实例化方法把一阶问题化为一系列命题逻辑中的可满足性问题来解决一阶逻辑的可满足问题，检查子句集的满足式映射中的阻塞是该方法

2、的关键．论文提出的子句搜索方法在判定子旬集可满足性的同时给出了一个模型从而得到满足式映射．格值逻辑的不完全可比性便于描述人类的思维、判断和决策．格值命题逻辑系统LP(X)于1993年建立，目前对LP(X)系统的自动推理研究主要是归结方法，论文讨论了它的tableau方法．常用的逻辑证明方法重点在于判定可满足性而不能给出符合人们阅读习惯的演绎过程．归结方法、语义表方法、相继式方法是定理证明中的常用方法，但是重点在于判定而不是演绎，论文探讨了相干命题逻辑系统R的试探法实现和相干自然推理系统NR的自然推理法实现，生成了类似于手工证明的可读证明．具体而言论文

3、的工作包括以下几方面：(1)提出了子旬搜索方法判定命题子句集的可满足性并给出可满足子句集的一个模型．子句搜索方法通过查找到子句集①不可扩展的子句C来判定①的可满足性．结合部分实例化方法将子句搜索方法提升至一阶，分离了谓词公式的结构和变量，从而提高合一算法的效率并节省了存贮空间．用正整数代表原子，负整数代表负文字，简化了算法实现．(2)提出了格值命题逻辑系统LP(X)的tableau方法，语义表中的公式都是受限蕴涵公式．通过引入Bounds∞、Bounds(X)和极大相容集证明了其正确性和完备性．对于真值域可直积分解的系统三，P(X)，讨论了其格直积分

4、解证明．(3)提出了后推试探证明方法并将演绎序列中的各公式组织成证明树从而产生了类似于手工证明的演绎序列．将公式转化为二叉树的形式存贮于动态数组中减小了公式冗余，用数组下标代表公式简化了实现．(4)提出了应用于自然推理方法的回溯方法．先从假设集出发构建证明树，再从树根节点逐层推导各公式的属性，实现了相干自然推理系统NR的类似手工证明的自然推理方法证明．综上所述，论文提出了判定子句集可满足性的子旬搜索方法并将其提升至一阶，提出了格值命题逻辑系统卯∞的tableau方法，提出了后推试探方法和回溯方法并实现了相干命题逻辑系统尺的可读证明，在理论和应用方面都

5、有积极意义．关键词：定理证明，自动推理，子句搜索方法，一阶逻辑，格值逻辑，tableau方法．试探方法，自然推理方法，可读证明．AbstractAutomatedtheoremprovingormechanicaltheoremprovingisconcemedwiththebuildingofcomputingsystemsthatautomatetheprocessofprovingtheorems．Sincethe1950sATPhasbeenoneofactiveresearchtopicsofcomputerscienceandsucces

6、sfullyusedinmathematics，hardtestandverification，softwaregenerationandverification，Dro-tocolverification，andartificialintelligence．Thepartialinstantiationmethodreducessatisfiabilityproblemsforfirst-orderlogictoaseriesofground-levelsatisfiabilityproblems．Findingouttheblockagesofs

7、atisfiermappingsforclausesetisnecessaryinthismethod．ClausesearchingmethodproposedbyIISnotonlydecidesthesatisfiabilityofclausesetbutalsopresentsamodelthenob-rainsasatisfiermapping．Lattice—valuedlogicisnotcompletelycomparableandpropertodescribingthinking，judginganddecision—making

8、．Lattice-valuedpropositionallogicsystemLP(X)isproposed