归结演绎推理

第三章归结演绎推理摘要：本文对归结对归结演绎推理进行了较为详细的介绍，描述了归结演绎推理的基本思路、使用步骤、并指明了其过程是完备的，还给出了运用归结原理进行归归结的具体例子，最后简单总结了其优缺点。关键词：归结，演绎，推理1知识背景人工智能是一门新兴的学科，推理技术是实现人工智能的基本技术之一，其中自然演绎推理是基于常用逻辑等价式以及常用逻辑蕴含式(统称推理规则)的推理技术，即从已知事实出发，利用推理规则进行推出结论的过程。这种推理过程与人类的思维过程极其相似，但其缺点是极易产生知识爆炸，推理过程中得到的中间结论按指数规律递增，对于复杂问题的推理不利，在计算机上实现起来存在诸多困难。而归结演绎推理是基于归结原理的在计算机上得到了较好实现的一种推理技术，是一种有效的机器推理方法。归结原理的出现,使得自动定理证明成为了可能，同时也使得人工智能技术向前迈进了一大步。2基本思路归结演绎方法是一种基于鲁滨逊（Robinson）归结原理的机器推理技术【1】。鲁滨逊归结原理也称作消解原理，是鲁滨逊于1965年在海伯伦（Herbrand）理论的基础上提出的一种基于逻辑的“反证法”。在人工智能中基本上几乎所有的问题都可以转化为一个定理证明问题。而定理证明的实质就是要从公式集12nP={PPP}，，出发推出结论G，即需要证明12nPPPG（）永真。要证明PG永真，若按定义来，需要证明PG在任何一个非空的个体域上都是永真的。这将是非常困难的，甚至是不可实现的。为此人们进行了大量的探索，后来发现可以采用反证法的思想，把关于永真性的证明转化为关于不可满足性的证明。即要证明PG永真，只要能够证明PG是不可满足的就可以了。在这一方面最有成效的的工作就是海伯伦理论和鲁滨逊归结原理。鲁滨逊归结原理使定理证明的机械化成为了现实。他们这些研究成果，在人工智能的发展史上都占有很重要的历史地位。(1)我们首先需证明式PGPG（）成立，永真性的证明可以化为不可满足性的证明。由命题逻辑的基本知识可得下表1-1：表1-1PGPGPG（）FFTTFTTTTFFFTTTT从上表可知：PGPG（），从而PG永真性的证明可以化为PG的不可满足性的证明。(2)要验证PG即12nPPPG（）不可满足，只需要验证以上公式中的任意一个子式不可满足即可。我们定义不包含任意文字的子句为空子句，空子句是永假的，不可满足的，一般记为NIL或□。由子句和空子句组成的集合称为子句集。在谓词逻辑中，任何一个谓词公式都可以通过应用等价关系及推理规则化成相应的子句集，且子句集无量词约束、元素只是文字的析取、否定符只作用于单个文字，元素间默认为和取。（3）归结：我们定义命题P为文字，P和P为互补文字。设C1和C2是子句集S中的任意两个子句，如果子句C1中的文字L1与C2中的文字L2互补，则可从C1和C2中分别消去L1和L2，并将两个子句余下的部分析取构成一个新子句C12。我们称这一过程为归结，C12为C1和C2的归结式，C1和C2为C12的亲本子句。即鲁滨逊归结原理的基本思路是：已知P，证明G，首先把欲证明的结论否定(G)，并加入前件知识构成子句集S（12n(PPPGS）），化子句集S；设法检验子句集S中是否有空子句，若含有空子句，则S是不可满足的；若不含有空子句，则继续使用归结运算，对S中的子句进行归结至导出空子句或不能继续归结为止。3使用步骤运用归结原理证明定理的过程称为归结反演。已知F，证明G的归结反演过程及步骤如下：（1）首先把欲证明的结论（目标公式）G否定得到G：（2）并把G加入公式集F中，得{F，G}；（3）把{F，G}化成子句集S；（4）运用归结原理对S中的子句进行归结，并将归结式加入S，反复进行，直到归结至导出空子句为止。4完备性归结原理的归结过程是完备的：因为子句集S是不可满足的，充要条件是存在一个从S到空子句的归结过程。我们知道：设C1和C2是子句集S中的任意两个子句，C12是C1和C2的归结式，若用C12代替C1和C2后，构成新的子句集S1，则由S1的不可满足性可以推出S的不可满足性，即：S1不可满足S不可满足。设C1和C2是子句集S中的任意两个子句，C12是C1和C2的归结式，若将C12添加到S中构成新的子句集S2，则由S2的不可满足性与S的不可满足性等价，即：S2不可满足S不可满足。进而我们可以利用新子句集S1和S2不可满足推出S不可满足。从而只要能从S归结出空子句，子句集S就是不可满足的；子句集S是不可满足的，就一定存在一个从S到空子句的归结过程。此归结具有完备性。5举例说明在谓词逻辑下求两个子句的归结式，和命题逻辑一样是消互补对，但需考虑变量的合一与置换。简单讨论一阶谓词逻辑描述下的归结推理方法，谓词逻辑的归结过程与命题逻辑的归结过程相比，其基本步骤相同，但每步的处理对象不同。谓词逻辑需要把由谓词构成的公式集化为子句集，必要时在得到归结式前要进行置换和合一。具体的谓词逻辑归结过程如下：(1)写出谓词关系公式(2)用反演法写出谓词表达式(3)化为Skolem标准形(4)求取子句集S(5)对S中可归结的子句做归结(6)归结式仍放入S中，反复归结过程(7)得到空子句(8)命题得证例如用归结原理求解“乐学生”问题：假设任何通过计算机考试并获奖的人都是快乐的，任何肯学习或幸运的人都可以通过所有的考试，张不肯学习但他是幸运的，任何幸运的人都能获奖。求证：张是快乐的。解：先将问题用谓词表示如下：R1:任何通过计算机考试并获奖的人都是快乐的(x)((Pass(x,computer)Win(x,prize))→Happy(x))R2:任何肯学习或幸运的人都可以通过所有考试(x)(y)(Study(x)Lucky(x)→Pass(x,y))R3:张不肯学习但他是幸运的Study(zhang)Lucky(zhang)R4:任何幸运的人都能获奖(x)(Luck(x)→Win(x,prize))结论张是快乐的的否定Happy(zhang)将上述谓词公式转化为子句集并进行归结如下：首先将每一个表示逻辑条件的谓词子句转换为子句集可以接受的Skolem标准形。由R1及逻辑转换公式PW→H=(PW)H,可得(1)Pass(x,computer)Win(x,prize)Happy(x)由R2可得(2)Study(y)Pass(y,z)(3)Lucky(u)Pass(u,v)由R3可得(4)Study(zhang)(5)Lucky(zhang)由R4可得(6)Lucky(w)Win(w，prize)由结论可得(7)Happy(zhang)结论的否定根据以上7条子句，归结如下：(8)Pass(w,computer)Happy(w)Luck(w)(1)，(6)归结，{w/x}(9)Pass(zhang,computer)Lucky(zhang)(8)，(7)归结，{zhang/w}(10)Pass(zhang,computer)(9)，(5)归结(11)Lucky(zhang)(10),(3)归结,{zhang/u,computer/v}(12)(11),(5)归结6优缺点总结定理证明的实质就是要对给出的（已知的）前提和结论，证明此前提推导出该结论这一事实是永恒的真理。这是非常困难的，几乎是不可实现的。要证明在一个论域上一个事件是永真的，就要证明在该域中的每一个点上该事实都成立。很显然，论域是不可数时，该问题不可能解决。即使可数，如果该轮域是无限的，问题也无法简单地解决。海伯伦采用了反证法的思想，将永真性的证明问题转化成为不可满足性的证明问题。海伯伦理论为自动定理证明奠定了理论基础，而鲁滨逊的归结原理使得自动定理证明得以实现。因此，归结推理方法在人工智能推理方法中有着很重要的历史地位。从某种意义上讲大部分人工智能问题都可以转化为一个定理证明问题。归结原理使定理证明的机械化成为了现实。当子句集很大时，归结过程会很复杂，一般的归结过程会很盲目，产生许多无用的归结式，更严重的是产生组合爆炸问题，所以还必须使用归结策略来进行控制，比如说删除策略或限制策略。参考文献：[1]尚富华.李军.人工智能及其运用[M].北京:石油工业出版社,2005.5.[2]廉师友.人工智能技术导论[M].西安:西安电子科技大学出版社,2000.[3]王永庆.人工智能原理与方法[M].西安:西安交通大学出版社,1998.[4]蔡自兴.徐光祐.人工智能及其运用[M].北京:清华大学出版社,2004.8.[5]朱福喜等.《人工智能原理》.武汉大学出版社.2002年[6]张仰森.黄改娟.《人工智能实用教程》.北京希望电子出版社.2002年