归结原理及其应用

《归结原理及其应用》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、万方数据第35卷(2007)第5期计算机与数字工程183归结原理及其应用4肖启莉1’肖启敏2’(浙江万里学院¨宁波315100)(空军第一航空学院2’信阳464000)摘要归结演绎推理是一种在计算机上得到较好实现的基于归结原理的推理技术，介绍归结原理的基本思想以及它在自动推理中的应用。关键词归结原理子句归结式中图分类号TPl81引言3归结原理及其应用推理技术是实现人工智能的基本技术之一，其中自然演绎推理是基于常用逻辑等价式以及常用逻辑蕴含式(统称推理规则)的推理技术，即从已知事实出发，利用推理规则

2、进行推出结论的过程。这种推理过程与人类的思维过程极其相似，但在计算机上实现起来存在诸多困难。而归结演绎推理是基于归结原理的在计算机上得到了较好实现的一种推理技术，是一种有效的机器推理方法。归结原理的出现，使得自动定理证明成为了可能，同时也使得人工智能技术向前迈进了一大步。2条件连接词及永真蕴含2．1条件连接词及其真值表图1真值表无论是命题逻辑还是谓词逻辑，均可用连接词把一些简单命题连接起来构成一个复合命题，以表示一个比较复杂的含义。其中条件连接词_：称为“条件”或“蕴含”。P—Q表示“P蕴含Q”，

3、即“如果P，则Q”。其真值表如图1。2．2永真蕴含定义1：对于谓词公式P和Q，如果P_÷Q永真，则称P永真蕴含Q，且称Q为P的逻辑结论，称P为Q的前提，记作PjQ。由以上定义l及真值表可以得出：结论1：即若Pjp，且结论的真值为假，则前提P为假。+收到本文时间：2006年10月25日作者简介：肖启莉，女，讲师，研究方向：AI、遗传算法。3．1归结原理归结原理是有鲁滨逊(J．A．Robinson)于1965年首先提出。其具体内容如下：归结原理：归结式是其亲本子句的逻辑结果。即假设有两个子旬c1、c2

4、，其归结式为R，则由归结原理可知：C1八C2一R永真。特别地，当C1=P，c2=～P时，R(C1，C2)=口，记作为空子句。由于空子句不能被任何解释所满足，所以其真值为假。由归结原理、c1／＼c2_口以及空子句即恒假子句可以得出以下结论。结论2：若两个子句c1、C2的归结式是空子句口，则c1、C2中至少有—个真值为假，即是不可满足的。3．2应用应用一：证明子句集是不可满足的定义2：子句集S是不可满足的，当且仅当全部子句的合取式是不可满足的由子句集不可满足的定义可知，只要证明子句集中有一个子句是不可

5、满足的即可。而由结论2可知，若对子句集(一次或多次)使用归结原理的过程中，若在某一步推出了空子句，则就推出子句集中至少有一个子句不可满足了矛盾，从而证明了子句集是不可满足的例1：证明子句集{PV～Q，～P，Q}是不可满足的。证：(1)PV～Q(2)～P(下转第187页)万方数据第35卷(2007)第5期计算机与数字工程187归树的建立中相关损失代价将比原先未经过_PCA处理时有所降低，并且随着节点数的增加过程中损失代价变化平稳。同时得到的分类的准确率和精度比只用CART方法要高。因此，应用PCA属

6、性归约和cART分类回归树的方法可以很好的应用于皮肤病学(de珊atology)的诊断分类中，另外由CART分类回归树生成的规则清晰而且容易理解。参考文献[1]秦欢，柴佩琪．基于决策树cART的中文文语转换系统语音合成单元的预选[J]．微型电脑应用，2004，20(5)：5～7[2]姚敏，沈斌，李明芳．基于多准则神经网络与分类回归树的电信行业异动客户识别系统[J]．系统工程理论(上接第183页)(3)Q(4)～Q(1)(2)(5)口(3)(4)在上例的证明过程中，由于(5)是(3)(4)的归结式，

7、且(5)的真值为假，由归结原理可知(3)(4)中至少有一个为假。假设(3)为假，由于(3)是子句集中的子句，所以由定义2可知子句集是不可满足的。若假设(4)为假，而(4)是(1)(2)的归结式，则(1)(2)中至少有一个为假，不管其中哪个为假，都证明了子句集是不可满足的。应用二：证明谓词公式是不可满足的定理：谓词公式G不可满足当且仅当其子句集s不可满足。由以上定理可知，要证明谓词公式是不可满足的只需将其转化成子句集，然后再对子句集进行归结，如果在某一时刻归结出了空子句，则就证明谓词公式是不可满足的

8、。例2：用归结原理证明R是P，(P八Q)一R，(sVu)一Q，u的逻辑结果证：由于前提条件P，(PAQ)_R，(SVU)一Q，u的真值为真，所以要证明R是其逻辑结果只需证明R真值为真，或者证明～R为假即可。即证明C=PA((P八Q)—，R)八((SVU)一Q)／＼U八～R是不可满足的。由谓词公式不可满足的充要条件可知，只要将与实践，2004，(5)：78～83[3]MingkunLi，shuoFeng，IshwarK．sethi，JasonLuciow，KeithWagner．Mi