基于谓词逻辑的归结原理研究

《基于谓词逻辑的归结原理研究》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、ComputerScienceandApplication计算机科学与应用,2011,1,51-56doi:10.4236/csa.2011.12011PublishedOnlineSeptember2011(http://www.hanspub.org/journal/csa/)TheStudyofResolutionPrincipleBasedonPredicateLogicYouyunAoSchoolofComputerandInformation,AnqingTeachersCollege,AnqingEmail:youy

2、un.ao@gmail.comReceived:May12th,2011;revised:Jul.11th,2011;accepted:Jul.25th,2011.Abstract:Resolutionprinciplebasedonpredicationlogicisaneffectiveapproachtoimplementingmachinereasoningorautomatedreasoning,andapplyingitcanprovetheoremsandextractanswerstoquestions.Thisp

3、aperanalyzesthetheoreticalbasisofresolutionprinciplebasedonpredicatelogic,anddiscussessomemethodsandproceduresofapplyingresolutionprinciplebasedonpredicatelogictotheoremprovingandproblem’sanswerextracting.Keywords:PredicateLogic;ResolutionPrinciple;ArtificialIntellige

4、nce;KnowledgeRepresentation基于谓词逻辑的归结原理研究敖友云安庆师范学院，计算机与信息学院，安庆Email:youyun.ao@gmail.com收稿日期：2011年5月12日；修回日期：2011年7月11日；录用日期：2011年7月25日摘要：基于谓词逻辑的归结原理是实现机器推理或自动推理的有效途径，利用它可以证明定理和提取问题答案。分析了基于谓词逻辑的归结原理的理论基础，并论述了将基于谓词逻辑的归结原理应用于定理证明和问题答案提取的方法及步骤。关键词：谓词逻辑；归结原理；人工智能；知识表示1.引言的提

5、出，为人类提供了一种简单易行的方法实现定理的证明和问题的求解，使定理证明可以在机器上机械谓词逻辑是在命题逻辑的基础上发展而来的，通[5,6]现实，是自动推理的重大突破。过引入量词，它比命题逻辑能更有效地表示和求证复本文从理论基础、求证问题的方法及步骤方面对杂问题。谓词逻辑采用形式化语言系统，通过一定的基于谓词逻辑的归结原理进行了研究。论文的组织结推理规则和控制策略，研究前提和结论之间的蕴涵关构如下：第2节分析了基于谓词逻辑的归结原理的理系。谓词逻辑具有严格的理论基础，可以保证推理过论基础；第3节讨论了将基于谓词逻辑的归结原理应程和

6、结论的正确性，同时它的形式化语言接近人类的用于定理证明和问题答案提取的方法及步骤；最后对[1]自然语言，容易为人类所理解和接受。全文进行了总结。经典的演绎推理系统具有证明过程自然、易于理解、推理规则丰富、推理过程灵活等优点，但也存在2.基于谓词逻辑的归结原理的理论基础推理过程中容易产生组合爆炸、证明方法难以判定等2.1.归结原理的基本思想[2,3][4]缺点。Robinson于1965年借助演绎推理反证法的思想提出了归结原理，它是一种形式单一、处理规则根据谓词公式和其对应的子句集在不可满足的意简单，可以在机器上实现的逻辑推理技术。

7、归结原理义下是等价的，为了证明谓词公式是不可满足的，可Copyright©2011HanspubCSA52敖友云基于谓词逻辑的归结原理研究以转化为证明其对应的子句集是不满足的。Robinson去存在量词后得到的Skolem范式并不唯一。一般地，[4]归结原理的基本思想描述如下：首先将待证明问题一个谓词公式与其Skolem范式并不等值，但若一个的结论的否定和问题的前提表示成谓词公式，然后将谓词公式是不可满足的，则其Skolem范式也一定是这些谓词公式转化为一个相应的子句集S，接下来按不可满足的，即引入Skolem函数并不影响原谓词公

8、一定的归结策略检验子句集S中是否含有空子句□，式的不可满足性。若含有空子句，则表明子句集S是不可满足的，问题2.3.置换与合一得到证明；否则继续在子句集S中选择合适的子句对进行归结，并将归结式并入子句集S中，直至推出空设C1和C2为两个不同的子句，