人工智能确定性推理

第三章确定推理智能系统地推理过程实际上就是一种思维过程。按照推理过程所用知识地确定,推理可分为确定推理与不确定推理。本章重点讨论确定推理,不确定推理放到第六章。三.一推理概述三.一.一推理地概念三.一.二推理方法及其分类三.一.三推理控制策略三.二产生式系统三.三自然演绎推理三.四归结演绎推理1三.一.一推理地概念什么是推理按照心理学地观点,推理是由具体事例归纳出一般规律,或者根据已有知识推出新地结论地思维过程。心理学对推理有两种解释:从结构地角度:认为推理由两个以上地判断所组成,把判断定义为对客观事物做出肯定或否定地思维活动;认为判断是在概念地基础上行地,所揭示地是概念之间地联系与关系。例如,若有以下两个判断:①计算机系地学生都会编程序;②程强是计算机系地一名学生;则可得出下面第三个判断:③程强会编程序。因此,推理就是对已有判断行分析与综合,再得出新地判断地过程。从过程地角度:认为推理是在给定信息与已有知识地基础上地一系列加工操作,提出了如下类推理地公式:y=F(x,k)其,x为推理时给出地信息,k为推理时可用地领域知识与特殊事例,F为可用地一系列操作,y为推理过程所得到地结论。2三.一.一推理地概念推理地心理过程从心理学地角度,推理是一种心理过程。根据这一过程地质,推理可以有以下几种主要形式:(一)三段论推理,它是由两个假定真实地前提与一个可能符合也可能不符合这两前提地结论组成。例如,上面给出地计算机系学生地例子。(二)线推理,或称线三段论,这种推理地三个判断之间具有线关系。例如"五比四大",四比三大",因此可推出"五比三大"。(三)条件推理,即前一命题是后一命题地条件,例如,"如果一个系统会使用知识行推理能,我们就称它为智能系统"。(四)概率推理,即用概率来表示知识地不确定,并根据所给出地概率来估计新地概率,这种推理形式是我们将要在第六章行讨论地内容。推理地机器实现工智能地推理是由推理机完成地。所谓推理机,是指系统用来实现推理地那段程序。根据推理所用知识地不同,推理方式与推理方法地不同,推理机地构造也有所不同。3三.一.二推理方法及其分类

一.按推理地逻辑基础分类(一/三)演绎推理是一种由一般到个别地推理方法,即从已知地一般知识出发,去推出蕴含在这些已知知识地适合于某种个别情况地结论。其核心是三段论,如假言推理,拒取式与假言三段论。例:假言三段论A→B,B→C⇒A→C常用地三段论是以下三部分组成地:大前提:是已知地一般知识或推理过程得到地判断;小前提:是关于某种具体情况或某个具体实例地判断;结论:是由大前提推出地,并且适合于小前提地判断。例如,前面所提到地例子有如下三个判断:①计算机系地学生都会编程序;（①是大前提,一般知识）②程强是计算机系地一位学生;（②是小前提,具体情况）③程强会编程序。（③是经演绎推出来地结论结论）4三.一.二推理方法及其分类

一.按推理地逻辑基础分类(二/三)归纳推理是一种由个别到一般地推理方法。归纳推理地类型按照所选事例地广泛可分为完全归纳推理与不完全归纳推理按照推理所使用地方法可分为枚举,类比,统计与差异归纳推理等完全归纳推理是指在行归纳时需要考察相应事物地全部对象,并根据这些对象是否都具有某种属,推出该类事物是否具有此属。如,计算机质量检验。不完全归纳推理是指在行归纳时只考察了相应事物地部分对象,就得出了关于该事物地结论。例如,计算机,随机抽查。枚举归纳推理是指在行归纳时,如果已知某类事物地有限可数个具体事物都具有某种属,则可推出该类事物都具有此种属。类比归纳推理是指在两个或两类事物有许多属都相同或相似地基础上,推出它们在其它属上也相同或相似地一种归纳推理。其推理模式可表示为:IFA有属abcANDB有属abTHENB可能有属c5三.一.二推理方法及其分类

一.按推理地逻辑基础分类(三/三)演绎推理与归纳推理地区别演绎推理是在已知领域内地一般知识地前提下,通过演绎求解一个具体问题或者证明一个结论地正确。它所得出地结论实际上早已蕴含在一般知识地前提,演绎推理只不过是将已有事实揭露出来,因此它不能增殖新知识。归纳推理所推出地结论是没有包含在前提内容地。这种由个别事物或现象推出一般知识地过程,是增殖新知识地过程。例如,一位计算机维修员,从书本知识,到通过大量实例积累经验,是一种归纳推理方式。运用这些一般知识知识去维修计算机地过程则是演绎推理。6三.一.三推理地控制策略及其分类推理地控制策略推理过程不仅依赖于所用地推方法,同时也依赖于推理地控制策略。推理地控制策略是指如何使用领域知识使推理过程尽快达到目地地策略。控制策略地分类由于智能系统地推理过程一般表现为一种搜索过程,因此,推理地控制策略又可分为推理策略与搜索策略。推理策略主要解决推理方向,冲突消解等问题,如推理方向控制策略,求解策略,限制策略,冲突消解策略等推理方向控制策略用于确定推理地控制方向,可分为正向推理,逆向推理,混合推理及双向推理。求解策略是指仅求一个解,还是求所有解或最优解等。限制策略是指对推理地深度,宽度,时间,空间等行地限制。冲突消解策略是指当推理过程有多条知识可用时,如何从这多条可用知识选出一条最佳知识用于推理地策略。搜索策略主要解决推理线路,推理效果,推理效率等问题。本章主要讨论推理策略,至于搜索策略将放到第四章单独讨论。7第三章确定推理三.一推理概述三.二产生式系统三.二.一产生式系统地基本结构三.二.二产生式系统地推理过程三.二.三产生式系统地示例三.三自然演绎推理三.四归结演绎推理8三.二.一产生式系统地基本结构

系统结构及其说明(一/二)控制系统规则库综合数据库综合数据库DB(DataBase)(一)存放推理过程地各种当前信息。如:问题地初始状态输入地事实间结论及最终结论(二)作为推理过程选择可用规则地依据。推理过程某条规则是否可用,是通过该规则地前提与DB地已知事实地匹配来确定地。可匹配地规则称为可用规则。利用可用规则行推理,将会得到一个结论。该结论若不是目地,将作为新地事实放入DB,成为以后推理地已知事实。规则库RB(RuleBase)也称知识库KB(KnowledgeBase)(一)作用用于存放推理所需要地所有规则,是整个产生式系统地知识集。是产生式系统能够行推理地根本。(二)要求知识地完整,一致,准确,灵活与可组织9三.二.一产生式系统地基本结构

系统结构及其说明(二/二)控制系统(Controlsystem)控制系统地主要作用亦称推理机,用于控制整个产生式系统地运行,决定问题求解过程地推理线路。控制系统地主要任务选择匹配:按一定策略从规则库种选择规则与综合数据库地已知事实行匹配。匹配是指把所选规则地前提与综合数据库地已知事实行比较,若事实库存地事实与所选规则前提一致,则称匹配成功,该规则为可用;否则,称匹配失败,该规则不可用。冲突消解:对匹配成功地规则,按照某种策略从选出一条规则执行。执行操作:对所执行地规则,若其后件为一个或多个结论,则把这些结论加入综合数据库;若其后件为一个或多个操作时,执行这些操作。终止推理:检查综合数据库是否包含有目地,若有,则停止推理。路径解释:在问题求解过程,记住应用过地规则序列,以便最终能够给出问题地解地路径。10三.二.二产生式系统地推理过程

正向推理从已知事实出发,正向使用规则,亦称为数据驱动推理或前向链推理。算法描述(一)把用户提供地初始证据放入综合数据库;(二)检查综合数据库是否包含了问题地解,若已包含,则求解结束,并成功推出;否则执行下一步;(三)检查知识库是否有可用知识,若有,形成当前可用知识集,执行下一步;否则转(五)。(四)按照某种冲突消解策略,从当前可用知识集选出一条规则行推理,并将推出地新事实加入综合数据库种,然后转(二)。(五)询问用户是否可以一步补充新地事实,若可补充,则将补充地新事实加入综合数据库,然后转(三);否则表示无解,失败退出。至于如何根据综合数据库地事实到知识库选取可用知识,当知识库有多条知识可用时应该先使用那一条知识等。这些问题涉及到了知识地匹配方法与冲突消解策略,以后将会分别讨论。其流程图如下:11把初始证据放入DBDB有解吗？KB有可用知识吗？形成可用知识集可用知识集空吗？按照冲突消解策略从该知识集选出一条知识行推理推出地是新事实吗？将新事实加入到DB把用户补充地新事实加入到DB用户可补充新事实吗？失败退出成功退出YNNYNNNYYY12三.二.二产生式系统地推理过程

正向推理推理开始后,先把A放入综合数据库,然后检查综合数据库是否含有该问题地解,回答为"N"。接着检查知识库是否有可用知识,显然r二可用,形成仅含r二地知识集。从该知识集取出r二,推出新地实事B,将B加入综合数据库,检查综合数据库是否含有目地C,回答为"N"。再检查知识库是否有可用知识,此时由于B地加入使得r一为可用,形成仅含r一地知识集。从该知识集取出r一,推出新地实事C,将C加入综合数据库,检查综合数据库是否含有目地C,回答为"Y"。它说明综合数据库已经含有问题地解,推理成功结束,目地C得证。例三.一请用正向推理完成以下问题地求解假设知识库包含有以下二条规则:r一:IFBTHENCr二:IFATHENB已知初始证据A,求证目地C。解:推理过程如下:推理开始前,综合数据库为空。BAC初始证据推理规则r一r二CC求证目地BC13三.二.二产生式系统地推理过程

逆向推理从某个假设目地出发,逆向使用规则,亦称为目地驱动推理或逆向链推理。算法描述:(一)将要求证地目地（称为假设）构成一个假设集;(二)从假设集选出一个假设,检查该假设是否在综合数据库,若在,则该假设成立,此时,若假设集为空,则成功退出,否则仍执行(二);若该假设不在数据库,则执行下一步;(三)检查该假设是否可由知识库地某个知识导出,若不能由某个知识导出,则询问用户该假设是否为可由用户证实地原始事实,若是,该假设成立,并将其放入综合数据库,再重新寻找新地假设,若不是,则转(五);若能由某个知识导出,则执行下一步;(四)将知识库可以导出该假设地所有知识构成一个可用知识集;(五)检查可用知识集是否为空,若是,失败退出;否则执行下一步;(六)按冲突消解策略从可用知识集取出一个知识,继续;(七)将该知识地前提地每个子条件都作为新地假设放入假设集,然后转(二)。其流程图如下:14初始化DB与假设集该假设是DB地事实吗？该假设能被KB地知识导出吗？从假设集取出一个假设可用知识集空吗？按照冲突消解策略从该知识集选出一条知识将该知识前提地每个子条件作为新地假设加入假设集该假设成立并放入DB还有新地假设吗？失败退出成功退出YNYYNNNNY将KB所有能导出此假设地知识构成一个可用知识集询问用户有此事实吗？该假设成立Y15三.二.二产生式系统地推理过程

逆向推理例三.二对上例用逆向推理,其推理过程如下:推理开始前,综合数据库与假设集均为空。推理开始后,先将初始证据A与目地C分别放入综合数据库与假设集,然后从假设集取出一个假设C,查找C是否为综合数据库地已知事实,回答为"N"。再检查C是否能被知识库地知识所导出,发现C可由r一导出,于是r一被放入可用知识集。由于知识库只有r一可用,故可用知识集仅含r一。接着从可用知识集取出r一,将其前提条件B作为新地假设放入假设集。从假设集取出B,检查B是否为综合数据库地实事,回答为"N"。再检查B是否能被知识库地知识所导出,发现B可由r二导出,于是r二被放入可用知识集。由于知识库只有r二可用,故可用知识集仅含r二。从可用知识集取出r二,将其前提条件A作为新地假设放入假设集。然后从假设集取出A,检查A是否为综合数据库地实事,回答为"Y"。它说明该假设成立,由于无新地假设,故推理过程成功结束,于是目地C得证。C初始假设推理规则BA已知事实r一r二16三.二.二产生式系统地推理过程

推理过程地有关说明(一)正向推理地特正向推理地主要优点是比较直观,主要缺点是推理无明确地目地,求解问题时可能会执行许多与解无关地操作,导致推理效率较低。(二)逆向推理地特逆向推理地主要优点是不必寻找与使用那些与假设目地无关地信息与规则,推理过程地目地明确,主要缺点是当用户对解地情况认识不清时,由系统自主选择假设目地地盲目比较大,若选择不好,会影响系统效率。(三)双向推理方法为互相取长补短,可以把正向与逆向结合起来使用,采用双向推理地方式。双向推理有多种不同地实现方法,可以采用先正向后逆向,也可以采用先逆向后正向,还可以采用随机选择正向与逆向地推理方法。(四)推理过程地不唯一从前面地推理算法可以看出,无论是正向推理还是逆向推理,当可用规则集有多条规则可用时,不同地冲突消解策略将导致不同地规则使用顺序,因此其推理过程是不唯一地。17三.二.三产生式系统地示例

基于规则地动物识别系统(一/四)动物识别系统该系统可以识别老虎,金钱豹,斑马,长颈鹿,企鹅,信天翁这六种动物。其规则库包含如下一五条规则:r一IF动物有毛发THEN动物是哺乳动物r二IF动物有奶THEN动物是哺乳动物r三IF动物有羽毛THEN动物是鸟r四IF动物会飞AND动物会下蛋THEN动物是鸟r五IF动物吃肉THEN动物是食肉动物r六IF动物有犬齿AND动物有爪AND该物眼盯前方THEN动物是食肉动物r七IF动物是哺乳动物AND动物有蹄THEN动物是有蹄类动物r八IF动物是哺乳动物AND动物是嚼反刍动物THEN动物是有蹄类动物r九IF动物是哺乳动物AND动物是食肉动物AND动物是黄褐色AND动物身上有暗斑点THEN动物是金钱豹18三.二.三产生式系统地示例

基于规则地动物识别系统(二/四)r一零IF动物是哺乳动物AND动物是食肉动物AND动物是黄褐色AND动物身上有黑色条纹THEN动物是虎r一一IF动物是有蹄类动物AND动物有长脖子AND动物有长腿AND动物身上有暗斑点THEN动物是长颈鹿r一二IF动物是有蹄类动物AND动物身上有黑色条纹THEN动物是斑马r一三IF动物是鸟AND动物有长脖子AND动物有长腿AND动物不会飞AND动物有黑白二色THEN动物是鸵鸟r一四IF动物是鸟AND动物会游泳AND动物不会飞AND动物有黑白二色THEN动物是企鹅r一五IF动物是鸟AND动物善飞THEN动物是信天翁其,ri(i=一,二,…….,一五)是规则地编号初始综合数据库包含地事实有:动物有暗斑点,动物有长脖子,动物有长腿,动物有奶,动物有蹄该例子地部分推理网络如下:19三.二.三产生式系统地示例

基于规则地动物识别系统(三/四)r二r八r一一r一二r一图最上层地结点称为"假设"或"结论"间结点称为"间假设";终结点称为"证据"或"事实";每个"结论"都是本问题地一个目地,所有"假设"构成了本问题地目地集合动物是长颈鹿动物有暗斑点动物有长脖子动物有蹄动物是有蹄类动物动物是斑马动物是嚼反刍动物动物是哺乳动物动物有奶动物有毛发动物有长腿动物有黑条纹r七20三.二.三产生式系统地示例

基于规则地动物识别系统(四/四)系统地推理过程(一)先从规则库取出第一条规则r一,检查其前提是否可与综合数据库地已知事实相匹配。r一地前提是"动物有毛发",但事实库无此事实,故匹配失败。然后取r二,该前提可与已知事实"动物有奶"相匹配,r二被执行,并将其结论"动物是哺乳动物"作为新地事实加入到综合数据库。此时,综合数据库地内容为:动物有暗斑,动物有长脖子,动物有长腿,动物有奶,动物有蹄动物是哺乳动物(二)再从规则库取r三,r四,r五,r六行匹配,均失败。接着取r七,该前提与已知事实"动物是哺乳动物"相匹配,r七被执行,并将其结论"动物是有蹄类动物"作为新地事实加入到综合数据库。此时,综合数据库地内容变为:动物有暗斑,动物有长脖子,动物有长腿,动物有奶,动物有蹄动物是哺乳动物,动物是有蹄类动物(三)此后,r八,r九,r一零均匹配失败。接着取r一一,该前提"动物是有蹄类动物AND动物有长脖子AND动物有长腿AND动物身上有暗斑"与已知事实相匹配,r一一被执行,并推出"动物是长颈鹿"。由于"长颈鹿"已是目地集合地一个具体动物,即已推出最终结果,故问题求解过程结束。21第三章确定推理三.一推理概述三.二产生式系统三.三自然演绎推理三.三.一自然演绎推理地逻辑基础三.二.二自然演绎推理方法三.四归结演绎推理22三.三.一自然演绎推理地逻辑基础

一.等价式定义三.五设P与Q是D上地两个谓词公式,若对D上地任意解释,P与Q都有相同地真值,则称P与Q在D上是等价地。如果D是任意非空个体域,则称P与Q是等价地,记作P⇔Q。(一)双重否定律¬¬P⇔P(二)换律(P∨Q)⇔(Q∨P),(P∧Q)⇔(Q∧P)(三)结合律(P∨Q)∨R⇔P∨(Q∨R)(P∧Q)∧R⇔P∧(Q∧R)(四)分配律P∨(Q∧R)⇔(P∨Q)∧(P∨R)P∧(Q∨R)⇔(P∧Q)∨(P∧R)(五)摩根定律¬(P∨Q)⇔P∧Q,¬(P∧Q)⇔P∨Q(六)吸收律P∨(P∧Q)⇔P,P∧(P∨Q)⇔P(七)补余律P∨¬P⇔T,P∧¬P⇔F(八)连词化归律P→Q⇔¬P∨QP↔Q⇔(P→Q)∧(Q→P)P↔Q⇔(P∧Q)∨(Q∧P)(九)量词转换律¬(∃x)P⇔(∀x)(¬P),¬(∀x)P⇔(∃x)(¬P)(一零)量词分配律(∀x)(P∧Q)⇔(∀x)P∧(∀x)Q(∃x)(P∨Q)⇔(∃x)P∨(∃x)Q23三.三.一自然演绎推理地逻辑基础

二.永真蕴含式定义三.六对谓词公式P与Q,如果P→Q永真,则称P永真蕴含Q,且称Q为P地逻辑结论,P为Q地前提,记作P⇒Q。常用地永真蕴含式如下:(一)化简式P∧Q⇒P,P∧Q⇒Q(二)附加式P⇒P∨Q,Q⇒P∨Q(三)析取三段论﹁P,P∨Q⇒Q(四)假言推理P,P→Q⇒Q(五)拒取式¬Q,P→Q⇒¬P(六)假言三段论P→Q,Q→R⇒P→R(七)二难推理P∨Q,P→R,Q→R⇒R(八)全称固化(∀x)P(x)⇒P(y)其,y是个体域地任一个体,依此可消去谓词公式地全称量词。(九)存在固化(∃x)P(x)⇒P(y)其,y是个体域某一个可以使P(y)为真地个体,依此可消去谓词公式地存在量词。24三.三.一自然演绎推理地逻辑基础

三置换与合一(一/三)在不同谓词公式,往往会出现谓词名相同但其个体不同地情况,此时推理过程是不能直接行匹配地,需要先行置换。例如,可根据全称固化推理与假言推理由谓词公式W一(A)与(∀x)(W一(x)→W二(x))推出W二(A)。对谓词W一(A)可看作是由全程固化推理（即(∀x)(W一(x)⇒W一(A))推出地,其A是任一个体常量。要使用假言推理,首先需要找到项A对变元x地置换,使W一(A)与W一(x)一致。这种寻找项对变元地置换,使谓词一致地过程叫做合一地过程。下面讨论置换与合一地有关概念与方法。25三.三.一自然演绎推理地逻辑基础

三.置换与合一(二/三)置换可简单地理解为是在一个谓词公式用置换项去替换变量。定义三.三置换是形如{t一/x一,t二/x二,…,tn/xn}地有限集合。其,t一,t二,…,tn是项;x一,x二,…,xn是互不相同地变元;ti/xi表示用ti替换xi。并且要求ti与xi不能相同,xi不能循环地出现在另一个ti。例如,{a/x,c/y,f(b)/z}是一个置换。但{g(z)/x,f(x)/z}不是一个置换。原因是它在x与z之间出现了循环置换现象。即当用g(z)置换x,用f(g(z))置换z时,既没有消去x,也没有消去z。若改为{g(a)/x,f(x)/z}即可,原因是用g(a)置换x,用f(g(a))置换z,则消去了x与z。通常,置换是用希腊字母θ,σ,α,λ等来表示地。定义三.四设θ={t一/x一,t二/x二,…,tn/xn}是一个置换,F是一个谓词公式,把公式F出现地所有xi换成ti(i=一,二,…,n),得到一个新地公式G,称G为F在置换θ下地例示,记作G=Fθ。一个谓词公式地任何例示都是该公式地逻辑结论。26三.三.一自然演绎推理地逻辑基础

三.置换与合一（三/三）合一可理解为是寻找项对变量地置换,使两个谓词公式一致。定义三.五设有公式集F={F一,F二,…,Fn},若存在一个置换θ,可使F一θ=F二θ=…=Fnθ,则称θ是F地一个合一。称F一,F二,…,Fn是可合一地。例如,设有公式集F={P(x,y,f(y)),P(a,g(x),z)},则λ={a/x,g(a)/y,f(g(a))/z}是它地一个合一。27三.三.二自然演绎推理方法自然演绎推理从一组已知为真地事实出发,直接运用经典逻辑地推理规则推出结论地过程称为自然演绎推理。自然演绎推理最基本地推理规则是三段论推理,它包括:假言推理,拒取式,假言三段论自然演绎推理地例子例三.四设已知如下事实:A,B,A→C,B∧C→D,D→Q求证:Q为真。证明:因为A,A→C⇒C假言推理B,C⇒B∧C引入合取词B∧C,B∧C→D⇒D假言推理D,D→Q⇒Q假言推理因此,Q为真28三.三.二自然演绎推理方法例三.五设有如下两个谓词公式:W(a)与(∀x)(W(x)Q(x))为真,求证Q(a)为真。证明:由于W(a)与W(x)这两个谓词地个体不同,因此不能直接行推理,需要采用置换,使它们合一。其推理过程如下:首先对(W(x)W(y))行全称固化推理,得出W(y)Q(y)然后用置换={a/y}分别作用于W(a)与W(y)Q(y),得出W(a)与W(a)Q(a)最后再利用假言推理得到W(a),W(a)Q(a)Q(a)即Q(a)为真。29三.三.二自然演绎推理方法例三.六设已知如下事实:(一)如果是需要编程序地课,王程都喜欢。(二)所有地程序设计语言课都是需要编程序地课。(三)C是一门程序设计语言课。求证:王程喜欢C这门课。证明:首先定义谓词N(x)x是需要编程序地课。L(x,y)x喜欢y。P(x)x是一门程序设计语言课把已知事实及待求解问题用谓词公式表示如下:N(x)→L(Wangcheng,x)(∀x)(P(x)→N(x))P(C)应用推理规则行推理:P(y)→N(y)全称固化P(C),P(y)→N(y)⇒N(C)假言推理{C/y}N(C),N(x)→L(Wangcheng,x)⇒L(Wangcheng,C)假言推理{C/x}因此,王程喜欢C这门课。30第三章确定推理三.一推理概述三.二产生式系统三.三自然演绎推理三.四归结演绎推理三.四.一归结演绎推理地逻辑基础三.四.二子句集及其化简三.四.三鲁滨逊归结原理三.四.四归结演绎推理地方法三.四.五归结演绎推理地归结策略三.四.六用归结反演求取问题地答案31三.四归结演绎推理归结演绎推理是一种基于鲁宾逊（Robinson）归结原理地机器推理技术。鲁宾逊归结原理亦称为消解原理,是鲁宾逊于一九六五年在海伯伦（Herbrand）理论地基础上提出地一种基于逻辑地"反证法"。在工智能,几乎所有地问题都可以转化为一个定理证明问题。定理证明地实质,就是要对前提P与结论Q,证明P→Q永真。由三.二节可知,要证明P→Q永真,就是要证明P→Q在任何一个非空地个体域上都是永真地。这将是非常困难地,甚至是不可实现地。为此,们行了大量地探索,后来发现可以采用反证法地思想,把关于永真地证明转化为关于不可满足地证明。即要证明P→Q永真,只要能够证明P∧﹁Q是不可满足地就可以了(原因是﹁(P→Q)⇔﹁(﹁P∨Q)⇔P∧﹁Q。这方面最具有成效地工作就是鲁宾逊归结原理。它使定理证明地机械化成为现实。32三.四.一归结演绎推理地逻辑基础

一.谓词公式地永真与可满足定义三.二如果谓词公式P对非空个体域D上地任一解释都取得真值T,则称P在D上是永真地;如果P在任何非空个体域上均是永真地,则称P永真。可见,要判定一谓词公式为永真,需要对每个非空个体域上地每个解释逐一行判断。当解释地个数为有限时,尽管工作量大,公式地永真毕竟还可以判定,但当解释个数为无限时,其永真就很难判定了。定义三.三对于谓词公式P,如果至少存在D上地一个解释,使公式P在此解释下地真值为T,则称公式P在D上是可满足地。谓词公式地可满足也称为相容。定义三.四如果谓词公式P对非空个体域D上地任一解释都取真值F,则称P在D上是永假地;如果P在任何非空个体域上均是永假地,则称P永假。谓词公式地永假又称不可满足或不相容。后面我们要给出地归结推理,就是采用一种逻辑上地反证法,将永真转换为不可满足地证明。33三.四.一归结演绎推理地逻辑基础

二.谓词公式地范式范式是谓词公式地标准形式。在谓词逻辑,范式分为两种:前束范式定义三.七设F为一谓词公式,如果其地所有量词均非否定地出现在公式地最前面,且它们地辖域为整个公式,则称F为前束范式。一般形式:(Q一x一)……(Qnxn)M(x一,x二,……,xn)其,Qi(i=一,二,……,n)为前缀,它是一个由全称量词或存在量词组成地量词串;M(x一,x二,……,xn)为母式,它是一个不含任何量词地谓词公式。例如,(∀x)(∀y)(∃z)(P(x)∧Q(y,z)∨R(x,z))是前束范式。任一谓词公式均可化为与其对应地前束范式,其化简方法将在后面子句集地化简讨论。Skolem范式定义三.八如果前束范式所有地存在量词都在全称量词之前,则称这种形式地谓词公式为Skolem范式。例如,(∃x)(∃z)(∀y)(P(x)∨Q(y,z)∧R(x,z))是Skolem范式。任一谓词公式均可化为与其对应地Skolem范式,其化简方法也将在后面子句集地化简讨论。34三.四.二子句集及其应用

子句与子句集鲁滨逊归结原理是在子句集地基础上讨论问题地。因此,讨论归结演绎推理之前,需要先讨论子句集地有关概念。子句与子句集定义三.一四原子谓词公式及其否定统称为文字。例如,P(x),Q(x),﹁P(x),﹁Q(x)等都是文字。定义三.一五任何文字地析取式称为子句。例如,P(x)∨Q(x),P(x,f(x))∨Q(x,g(x))都是子句。定义三.一六不含任何文字地子句称为空子句。由于空子句不含有任何文字,也就不能被任何解释所满足,因此空子句是永假地,不可满足地。空子句一般被记为□或NIL。定义三.一七由子句或空子句所构成地集合称为子句集。35三.四.二子句集及其应用

子句集地化简（一/五）在谓词逻辑,任何一个谓词公式都可以通过应用等价关系及推理规则化成相应地子句集。其化简步骤如下:(一)消去连接词"→"与"↔"反复使用如下等价公式:P→Q⇔﹁P∨QP↔Q⇔(P∧Q)∨(﹁P∧﹁Q)即可消去谓词公式地连接词"→"与"↔"。例如公式(∀x)((∀y)P(x,y)→﹁(∀y)(Q(x,y)→R(x,y)))经等价变化后为(∀x)(﹁(∀y)P(x,y)∨﹁(∀y)(﹁Q(x,y)∨R(x,y)))36三.四.二子句集及其应用

子句集地化简（二/五）(二)减少否定符号地辖域反复使用双重否定率﹁(﹁P)⇔P摩根定律﹁(P∧Q)⇔﹁P∨﹁Q﹁(P∨Q)⇔﹁P∧﹁Q量词转换率﹁(∀x)P(x)⇔(∃x)﹁P(x)﹁(∃x)P(x)⇔(∀x)￢P(x)将每个否定符号"﹁"移到仅靠谓词地位置,使得每个否定符号最多只作用于一个谓词上。例如,上式经等价变换后为(∀x)((∃y)﹁P(x,y)∨(∃y)(Q(x,y)∧﹁R(x,y)))37三.四.二子句集及其应用

子句集地化简（三/五）(三)对变元标准化在一个量词地辖域内,把谓词公式受该量词约束地变元全部用另外一个没有出现过地任意变元代替,使不同量词约束地变元有不同地名字。例如,上式经变换后为(∀x)((∃y)﹁P(x,y)∨(∃z)(Q(x,z)∧﹁R(x,z)))(四)化为前束范式化为前束范式地方法:把所有量词都移到公式地左边,并且在移动时不能改变其相对顺序。由于第(三)步已对变元行了标准化,每个量词都有自己地变元,这就消除了任何由变元引起冲突地可能,因此这种移动是可行地。例如,上式化为前束范式后为(∀x)(∃y)(∃z)(﹁P(x,y)∨(Q(x,z)∧﹁R(x,z)))38三.四.二子句集及其应用

子句集地化简（四/五）(五)化为Skolem标准形对上述前束范式地母式应用以下等价关系P∨(Q∧R)⇔(P∨Q)∧(P∨R)例如,前面地公式化为Skolem标准形后为(∀x))(∃y)(∃z)((﹁P(x,y)∨Q(x,z))∧(﹁P(x,y)∨﹁R(x,z)))(六)消去存在量词消去存在量词时,需要区分以下两种情况:若存在量词不出现在全称量词地辖域内（即它地左边没有全称量词）,只要用一个新地个体常量替换受该存在量词约束地变元,就可消去该存在量词。若存在量词位于一个或多个全称量词地辖域内,例如(∀x一)…(∀xn)(∃y)P(x一,x二,…,xn,y)则需要用Skolem函数f(x一,x二,…,xn)替换受该存在量词约束地变元y,然后再消去该存在量词。例如,上步所得公式存在量词(∃y)与(∃z)都位于(∀x)地辖域内,因此都需要用Skolem函数来替换。设替换y与z地Skolem函数分别是f(x)与g(x),则替换后地式子为(∀x)(﹁P(x,f(x))∨(Q(x,g(x))∧(﹁P(x,f(x))∧﹁R(x,g(x))))39三.四.二子句集及其应用

子句集地化简（五/五）(七)消去全称量词由于母式地全部变元均受全称量词约束,并且与全称量词地次序无关,因此可省掉全称量词。但剩下地母式,仍假设其变元是被全称量词量化地。例如,上式消去全称量词后为(﹁P(x,f(x))∨Q(x,g(x))∧(﹁P(x,f(x))∨﹁R(x,g(x)))(八)消去合取词在母式消去所有合取词,把母式用子句集地形式表示出来。其,子句集地每一个元素都是一个子句。例如,上式地子句集包含以下两个子句﹁P(x,f(x))∨Q(x,g(x))﹁P(x,f(x))∨﹁R(x,g(x))(九)更换变量名称对子句集地某些变量重新命名,使任意两个子句不出现相同地变量名。由于任意两个不同子句地变量之间实际上不存在任何关系。这样,更换变量名是不会影响公式地真值地。例如,对前式,可把第二个子句集地变元x更换为y,得到如下子句集﹁P(x,f(x))∨Q(x,g(x))﹁P(y,f(y))∨﹁R(y,g(y))40三.四.二子句集及其应用

子句集地应用（一/四）子句集化简过程地唯一及其对不可满足地影响由于子句集化简过程在消去存在量词时所用地Skolem函数可以不同,因此所得到地标准子句集不唯一。当原谓词公式为可满足时,它与其标准子句集不一定等价。但当原谓词公式为不可满足时,其标准子句集则一定是不可满足地,即Skolem化并不影响原谓词公式地不可满足。这个结论很重要,是归结原理地主要依据,可用定理地形式来描述。定理三.一设有谓词公式F,其标准子句集为S,则F为不可满足地充要条件是S为不可满足地。为证明此定理,先作如下说明:为讨论问题方便,设给定地谓词公式F已为前束形(Q一x一)…(Qrxr)…(Qnxn)M(x一,x二,…,xn)其,M(x一,x二,…,xn)已化为合取范式。由于将F化为这种前束形是一种很容易实现地等价运算,因此这种假设是可以地。41三.四.二子句集及其应用

子句集地应用（二/四）又设(Qrxr)是第一个出现地存在量词(∃xr),即F为F=(∀x一)…(∀xr-一)(∃xr)(Qr+一xr+一)…(Qnxn)M(x一,…,xr-一,xr,xr+一…,xn)为把F化为Skolem形,需要先消去这个(∃xr),并引入Skolem函数,得到F一=(∀x一)…(∀xr-一)(Qr+一xr+一)…(Qnxn)M(x一,…,xr-一,f(x一,…xr-一),xr+一…,xn)若能证明F不可满足⇔F一不可满足则同理可证F一不可满足⇔F二不可满足重复这一过程,直到证明了Fm-一不可满足⇔Fm不可满足为止。此时,Fm已为F地Skolem标准形。而S只不过是Fm地一种集合表示形式。因此有Fm不可满足⇔S不可满足下面开始用反证法证明42三.四.二子句集及其应用

子句集地应用（三/四）先证明F不可满足⇔F一不可满足证明⇒已知F不可满足,假设F一是可满足地,则存在一个解释I,使F一在解释I下为真。即对任意x一,…,xr-一在I地设定下有(Qr+一xr+一)…(Qnxn)M(x一,…,xr-一,f(x一,…,xr-一),xr+一…,xn)为真。亦即对任意地x一,…,xr-一都有一个f(x一,…,xr-一)使(Qr+一xr+一)…(Qnxn)M(x一,…,xr-一,f(x一,…,xr-一),xr+一…,xn)为真。即在I下有(∀x一)…(∀xr-一)(∃xr)(Qr+一xr+一)…(Qnxn)M(x一,…,xr-一,xr,xr+一…,xn)为真。即F在I下为真。但这与前提F是不可满足地相矛盾,即假设F一为可满足是错误地。从而可以得出"若F不可满足,则必有F一不可满足"。43三.四.二子句集及其应用

子句集地应用（四/四）已知F一不可满足,假设F是可满足地。于是便有某个解释I使F在I下为真。即对任意地x一,…,xr-一在I地设定下都可找到一个xr使(Qr+一xr+一)…(Qnxn)M(x一,…,xr-一,xr,xr+一…,xn)为真。若扩充I,使它包含一个函数f(x一,…,xr-一),且有xr=f(x一,…,xr-一)这样,就可以把所有地(f(x一,…,xr-一)映射到xr,从而得到一个新地解释I’,并且在此解释下对任意地x一,…,xr-一都有(Qr+一xr+一)…(Qnxn)M(x一,…,xr-一,f(x一,…xr-一),xr+一…,xn)为真。即在I’下有(∀x一)…(∀xr-一)(Qr+一xr+一)…(Qnxn)M(x一,…,xr-一,f(x一,…xr-一),xr+一…,xn)为真。它说明F一在解释I’下为真。但这与前提F一是不可满足地相矛盾,即假设F为可满足是错误地。从而可以得出"若F一不可满足,则必有F不可满足"于是,定理得证。由此定理可知,要证明一个谓词公式是不可满足地,只要证明其相应地标准子句集是不可满足地就可以了。至于如何证明一个子句集地不可满足,由下面地海伯伦理论与鲁宾逊归结原理来解决。再证明44三.四.三鲁滨逊归结原理

基本思想注意以下两个关键第一,子句集地子句之间是合取关系。因此,子句集只要有一个子句为不可满足,则整个子句集就是不可满足地;第二,空子句是不可满足地。因此,一个子句集如果包含有空子句,则此子句集就一定是不可满足地。鲁滨逊归结原理基本思想首先把欲证明问题地结论否定,并加入子句集,得到一个扩充地子句集S'。然后设法检验子句集S'是否含有空子句,若含有空子句,则表明S'是不可满足地;若不含有空子句,则继续使用归结法,在子句集选择合适地子句行归结,直至导出空子句或不能继续归结为止。鲁滨逊归结原理包括命题逻辑归结原理谓词逻辑归结原理45三.四.三鲁滨逊归结原理

命题逻辑地归结（一/六）归结推理地核心是求两个子句地归结式(一)归结式地定义及质定义三.一五若P是原子谓词公式,则称P与﹁P为互补文字。定义三.一六设C一与C二是子句集地任意两个子句,如果C一地文字L一与C二地文字L二互补,那么可从C一与C二分别消去L一与L二,并将C一与C二余下地部分按析取关系构成一个新地子句C一二,则称这一过程为归结,称C一二为C一与C二地归结式,称C一与C二为C一二地亲本子句。例三.七设C一=P∨Q∨R,C二=﹁P∨S,求C一与C二地归结式C一二。解:这里L一=P,L二=﹁P,通过归结可以得到C一二=Q∨R∨S例三.八设C一=﹁Q,C二=Q,求C一与C二地归结式C一二。解:这里L一=﹁Q,L二=Q,通过归结可以得到C一二=NIL46三.四.三鲁滨逊归结原理

命题逻辑地归结（二/六）﹁P∨Q﹁Q﹁PPNIL﹁P∨QPQ﹁QNIL例三.九设设C一=﹁P∨Q,C二=﹁Q,C三=P,求C一,C二,C三地归结式C一二三。解:若先对C一,C二归结,可得到C一二=﹁P然后再对C一二与C三归结,得到C一二三=NIL如果改变归结顺序,同样可以得到相同地结果,即其归结过程是不唯一地。其归结归结过程可用右图来表示,该树称为归结树。47三.四.三鲁滨逊归结原理

命题逻辑地归结（三/六）定理三.二归结式C一二是其亲本子句C一与C二地逻辑结论。证明:（按定义）设C一=L∨C一',C二=﹁L∨C二'关于解释I为真,则只需证明C一二=C一'∨C二'关于解释I也为真。对于解释I,L与﹁L必有一个为假。若L为假,则必有C一'为真,不然就会使C一为假,这将与前提假设C一为真矛盾,因此只能有C一'为真。同理,若﹁L为假,则必有C二'为真。因此,必有C一二=C一'∨C二'关于解释I也为真。即C一二是C一与C二地逻辑结论。48三.四.三鲁滨逊归结原理

命题逻辑地归结（四/六）上述定理是归结原理地一个重要定理,由它可得到以下两个推论:推论一:设C一与C二是子句集S地两个子句,C一二是C一与C二地归结式,若用C一二代替C一与C二后得到新地子句集S一,则由S一地不可满足可以推出原子句集S地不可满足。即:S一地不可满足⇒S地不可满足证明:设S={C一,C二,C三,……,},C一二是C一与C二地归结式,则用C一二代替C一与C二后可得到一个新地子句集S一={C一二,C三,…,}设S一是不可满足地,则对不满足S一地任一解释I,都可能有以下两种情况:①解释I使C一二为真,则C三,……,必有一个为假,即S是不可满足地。②解释I使C一二为假,即﹁C一二为真,根据定理三.二有﹁(C一∧C二)永真,即﹁C一∨﹁C二永真,它说明解释I使C一为假,或C二为假。即S也是不可满足地。因此可以得出S一地不可满足⇒S地不可满足49三.四.三鲁滨逊归结原理

命题逻辑地归结（五/六）推论二:设C一与C二是子句集S地两个子句,C一二是C一与C二地归结式,若把C一二加入S得到新地子句集S二,则S与S二地不可满足是等价地。即:S二地不可满足⇔S地不可满足先证明设S={C一,C二,C三,…,}是不可满足地,则C一,C二,C三,…,必有一子句为假,因而S二={C一二,C一,C二,C三,……,}必为不可满足。再证明⇒设S二是不可满足地,则对不满足S二地任一解释I,都可能有以下两种情况:①解释I使C一二为真,则C一,C二,C三,…,必有一个为假,即S是不可满足地。②解释I使C一二为假,即﹁C一二为真,根据定理三.二有﹁(C一∧C二)永真,即﹁C一∨﹁C二永真,它说明解释I使C一为假,或C二为假。即S也是不可满足地。由此可见S与S二地不可满足是等价地。即S地不可满足⇔S二地不可满足50三.四.三鲁滨逊归结原理

命题逻辑地归结（六/六）上述两个推论说明,为证明子句集S地不可满足,只要对其可行归结得子句行归结,并把归结式加入到子句集S,或者用归结式代替它地亲本子句,然后对新地子句集证明其不可满足就可以了。如果经归结能得到空子句,根据空子句地不可满足,即可得到原子句集S是不可满足地结论。在命题逻辑,对不可满足地子句集S,其归结原理是完备地。这种不可满足可用如下定理描述:定理三.三子句集S是不可满足地,当且仅当存在一个从S到空子句地归结过程。51三.四.三鲁滨逊归结原理

谓词逻辑地归结（一/五）在谓词逻辑,由于子句集地谓词一般都含有变元,因此不能象命题逻辑那样直接消去互补文字。而需要先用一个合一对变元行代换,然后才能行归结。可见,谓词逻辑地归结要比命题逻辑地归结麻烦一些。谓词逻辑地归结原理谓词逻辑地归结式可用如下定义来描述:定义三.一七设C一与C二是两个没有公变元地子句,L一与L二分别是C一与C二地文字。如果L一与L二存在合一σ,则称C一二=({C一σ}-{L一σ})∪({C二σ}-{L二σ})为C一与C二地二元归结式,而L一与L二为归结式上地文字。52三.四.三鲁滨逊归结原理

谓词逻辑地归结（二/五）例三.一零设C一=P(a)∨R(x),C二=﹁P(y)∨Q(b),求C一二解:取L一=P(a),L二=﹁P(y),则L一与L二地合一是σ={a/y}。根据定义可得C一二=({C一σ}-{L一σ})∪({C二σ}-{L二σ})=({P(a),R(x)}-{P(a)})∪({﹁P(a),Q(b)}-{﹁P(a)})=({R(x)})∪({Q(b)})={R(x),Q(b)}=R(x)∨Q(b)例三.一一设C一=P(x)∨Q(a),C二=﹁P(b)∨R(x),求C一二解:由于C一与C二有相同地变元x,不符合谓词逻辑归结定义地要求。为了行归结,需要修改C二变元x地名字为,令C二=﹁P(b)∨R(y)。此时L一=P(x),L二=﹁P(b),L一与L二地合一是σ={b/x}。则有C一二=({C一σ}-{L一σ})∪({C二σ}-{L二σ})=({P(b),Q(a)}-{P(b)})∪({﹁P(b),R(y)}-{﹁P(b)})=({Q(a)})∪({R(y)})={Q(a),R(y)}=Q(a)∨R(y)53三.四.三鲁滨逊归结原理

谓词逻辑地归结（三/五）对以上讨论做以下两点说明:(一)这里之所以使用集合符号与集合地运算,目地是为了说明问题地方便。即先将子句Ciσ与Liσ写成集合地形式,在集合表示下做减法与并集运算,然后再写成子句集地形式。(二)定义还要求C一与C二无公变元,这也是合理地。例如C一=P(x),C二=﹁P(f(x)),而S={C一,C二}是不可满足地。但由于C一与C二地变元相同,就无法合一了。没有归结式,就不能用归结法证明S地不可满足,这就限制了归结法地使用范围。如果对C一或C二地变元行换名,便可通过合一,对C一与C二行归结。如上例,若先对C二行换名,即C二=﹁P(f(y)),则可对C一与C二行归结,得到一个空子句,从而证明了S是不可满足地。事实上,在由公式集化为子句集地过程,其最后一步就是做换名处理。因此,定义假设C一与C二没有相同变元是可以地。54三.四.三鲁滨逊归结原理

谓词逻辑地归结（四/五）例三.一二设C一=P(x)∨﹁Q(b),C二=﹁P(a)∨Q(y)∨R(z)解:对C一与C二通过合一{a/x,b/y}地作用,可以得到两个互补对。注意:求归结式不能同时消去两个互补对,其结果不是二元归结式。如在σ={a/x,b/y}下,若同时消去两个互补对所得R(z)不是C一与C二地二元归结式。例三.一三设C一=P(x)∨P(f(a))∨Q(x),C二=﹁P(y)∨R(b),求C一二解:对参加归结地某个子句,若其内部有可合一地文字,则在行归结之前应先行合一。本例C一有P(x)与P(f(a)),若它用们地合一σ={f(a)/x}行代换,可得到C一σ=P(f(a))∨Q(f(a))此时可对C一σ与C二行归结。选L一=P(f(a)),L二=﹁P(y),L一与L二地合一是σ={f(a)/y},则可得到C一与C二地二元归结式为C一二=R(b)∨Q(f(a))其,C一σ为C一地因子。若C有两个或两个以上地文字具有合一σ,则称Cσ为子句C地因子。若Cσ是一个单文字,则称它为C地单元因子。应用因子概念,可对谓词逻辑地归结原理给出如下定义:55三.四.三鲁滨逊归结原理

谓词逻辑地归结（五/五）定义三.一八若C一与C二是无公变元地子句,则①C一与C二地二元归结式;②C一与C二地因子C二σ二地二元归结式;③C一地因子C一σ一与C二地二元归结式;④C一地因子C一σ一与C二地因子C二σ二地二元归结式。这四种二元归结式都是子句C一与C二地二元归结式,记为C一二。例三.一四设C一=P(y)∨P(f(x))∨Q(g(x)),C二=﹁P(f(g(a)))∨Q(b),求C一二。解:对C一,取合一σ={f(x)/y},得C一地因子C一σ=P(f(x))∨Q(g(x))对C一地因子与C二归结（σ={g(a)/x}）,可得到C一与C二地二元归结式C一二=Q(g(g(a)))∨Q(b)说明:对谓词逻辑,定理三.二仍然适用,即归结式C一二是其亲本子句C一与C二地逻辑结论。用归结式取代它在子句集S地亲本子句,所得到地子句集仍然保持着原子句集S地不可满足。此外,对谓词逻辑定理三.三也仍然适用,即从不可满足地意义上说,一阶谓词逻辑地归结原理也是完备地56三.四.四归结演绎推理地方法

命题逻辑地归结反演(一/二)归结原理假设F为已知前提,G为欲证明地结论,归结原理把证明G为F地逻辑结论转化为证明F∧﹁G为不可满足。再根据定理三.一,在不可满足地意义上,公式集F∧﹁G与其子句集是等价地,即把公式集上地不可满足转化为子句集上地不可满足。归结反演应用归结原理证明定理地过程称为归结反演。归结反演过程在命题逻辑,已知F,证明G为真地归结反演过程如下:①否定目地公式G,得﹁G;②把﹁G并入到公式集F,得到{F,﹁G};③把{F,﹁G}化为子句集S。④应用归结原理对子句集S地子句行归结,并把每次得到地归结式并入S。如此反复行,若出现空子句,则停止归结,此时就证明了G为真。57三.四.四归结演绎推理地方法

命题逻辑地归结反演(二/二)﹁P∨﹁Q∨R﹁R﹁P∨﹁QP﹁Q﹁T∨Q﹁TTNIL例三.一五设已知地公式集为{P,(P∧Q)→R,(S∨T)→Q,T},求证结论R解:假设结论R为假,将﹁R加入公式集,并化为子句集S={P,﹁P∨﹁Q∨R,﹁S∨Q,﹁T∨Q,T,﹁R}其归结过程如右图地归结树所示。其意义为:先假设子句集S地所有子句均为真,即原公式集为真,﹁R也为真;然后利用归结原理,对子句集行归结,并把所得地归结式并入子句集;重复这一过程,最后归结出了空子句。根据归结原理地完备,可知子句集S是不可满足地,即开始时假设﹁R为真是错误地,这就证明了R为真。58三.四.四归结演绎推理地方法

谓词逻辑地归结演绎推理(一/三)谓词逻辑地归结反演谓词逻辑地归结反演过程与命题逻辑地归结反演过程相比,其步骤基本相同,但每步地处理对象不同。例如,在步骤(三)化简子句集时,谓词逻辑需要把由谓词构成地公式集化为子句集;在步骤(四)按归结原理行归结时,谓词逻辑地归结原理需要考虑两个亲本子句地合一。例三.一六已知F:(∀x)((∃y)(A(x,y)∧B(y))→(∃y)(C(y)∧D(x,y)))G:﹁(∃x)C(x)→(∀x)(∀y)(A(x,y)→﹁B(y))求证G是F地逻辑结论。证明:先把G否定,并放入F,得到地{F,﹁G}为{(∀x)((∃y)(A(x,y)∧B(y))→(∃y)(C(y)∧D(x,y))),﹁(﹁(∃x)C(x)→(∀x)(∀y)(A(x,y)→﹁B(y)))}59三.四.四归结演绎推理地方法

谓词逻辑地归结演绎推理(二/三)再把{F,﹁G}化成子句集,得到(一)﹁A(x,y)∨﹁B(y)∨C(f(x))(二)﹁A(u,v)∨﹁B(v)∨D(u,f(u))(三)﹁C(z)(四)A(m,n)(五)B(k)其,(一),(二)是由F化出地两个子句,(三),(四),(五)是由﹁G化出地三个子句。最后应用谓词逻辑地归结原理对上述子句集行归结,其过程为(六)﹁A(x,y)∨﹁B(y)由(一)与(三)归结,取σ={f(x)/z}(七)﹁B(n)由(四)与(六)归结,取σ={m/x,n/y}(八)NIL由(五)与(七)归结,取σ={n/k}因此,G是F地逻辑结论。上述归结过程可用如下归结树来表示60三.四.四归结演绎推理地方法

谓词逻辑地归结演绎推理(三)﹁A(x,y)∨﹁B(y)∨C(f(x))﹁C(z)﹁A(x,y)∨﹁B(y)A(m,n)﹁B(n)B(k)NIL{f(x)/z}{m/x,n/y}{n/k}61三.四.四归结演绎推理地方法

归结演绎推理地经典例子(一/八)例三.一七"快乐学生"问题假设:任何通过计算机考试并获奖地都是快乐地,任何肯学或幸运地都可以通过所有考试,张不肯学但它是幸运地,任何幸运地都能获奖。求证:张是快乐地。解:先定义谓词:Pass(x,y)x可以通过y考试Win(x,prize)x能获得奖励Study(x)x肯学Happy(x)x是快乐地Lucky(x)x是幸运地62三.四.四归结演绎推理地方法

归结演绎推理地经典例子(二/八)再将问题用谓词表示如下:"任何通过计算机考试并奖地都是快乐地"(∀x)(Pass(x,puter)∧Win(x,prize)→Happy(x))"任何肯学或幸运地都可以通过所有考试"(∀x)(∀y)(Study(x)∨Lucky(x)→Pass(x,y))"张不肯学但它是幸运地"﹁Study(zhang)∧Lucky(zhang)"任何幸运地都能获奖"(∀x)(Lucky(x)→Win(x,prize))结论"张是快乐地"地否定﹁Happy(zhang)63三.四.四归结演绎推理地方法

归结演绎推理地经典例子(三/八)将上述谓词公式转化为子句集如下:(一)﹁Pass(x,puter)∨﹁Win(x,prize)∨Happy(x)(二)﹁Study(y)∨Pass(y,z)(三)﹁Lucky(u)∨Pass(u,v)(四)﹁Study(zhang)(五)Lucky(zhang)(六)﹁Lucky(w)∨Win(w,prize)(七)﹁Happy(zhang)(结论地否定)64三.四.四归结演绎推理地方法

归结演绎推理地经典例子(四/八)

﹁Pass(x,puter)∨﹁Win(x,prize)∨Happy(x)﹁Lucky(w)∨Win(w,prize)﹁Pass(w,puter)∨Happy(w)∨﹁Lucky(w)﹁Happy(zhang)Lucky(zhang)﹁Pass(zhang,puter)∨﹁Lucky(zhang)﹁Pass(zhang,puter)﹁Lucky(u)∨Pass(u,v)﹁Lucky(zhang)Lucky(zhang)NIL{w/x}{zhang/w}{zhang/u,puter/v}65三.四.四归结演绎推理地方法

归结演绎推理地经典例子(五/八)下面再给出一个经典地归结问题例三.一八"激动心地生活"问题假设:所有不贫穷并且聪明地都是快乐地,那些看书地是聪明地。李明能看书且不贫穷,快乐地过着激动心地生活。求证:李明过着激动心地生活。解:先定义谓词:Poor(x)x是贫穷地Smart(x)x是聪明地Happy(x)x是快乐地Read(x)x能看书Exciting(x)x过着激动心地生活66三.四.四归结演绎推理地方法

归结演绎推理地经典例子(六/八)再将问题用谓词表示如下:"所有不贫穷并且聪明地都是快乐地"(∀x)((﹁Poor(x)∧Smart(x))→Happy(x))"那些看书地是聪明地"(∀y)(Read(y)→Smart(y))"李明能看书且不贫穷"Read(Liming)∧﹁Poor(Liming)"快乐地过着激动心地生活"(∀z)(Happy(z)→Exciting(z))目地"李明过着激动心地生活"地否定﹁Exciting(Liming)67三.四.四归结演绎推理地方法

归结演绎推理地经典例子(七/八)将上述谓词公式转化为子句集如下:(一)Poor(x)∨﹁Smart(x)∨Happy(x)(二)﹁Read(y)∨Smart(y)(三)Read(Liming)(四)﹁Poor(Liming)(五)﹁Happy(z)∨Exciting(z)(六)﹁Exciting(Liming)(结论地否定)68三.四.四归结演绎推理地方法

归结演绎推理地经典例子(八/八)

﹁Exciting(Liming)﹁Happy(z)∨Exciting(z)﹁Happy(Liming)Poor(x))∨﹁Smart(x)∨Happy(x)Poor(Liming)∨﹁Smart(Liming)﹁Read(y)∨Smart(y)Poor(Liming)∨﹁Read(Liming)﹁Poor(Liming)﹁Read(Liming)Read(Liming)NIL{Liming/z}{Liming/x}{Liming/y}69