《三章谓词演算与消解归结原理.ppt》由会员分享，可在线阅读，更多相关《三章谓词演算与消解归结原理.ppt（79页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。
1、1DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial IntelligenceSpring三章谓词演算与消解归结原理 Still waters run deep.流静水深流静水深,人静心深人静心深 Where there is life,there is hope。有生命必有希望。有生命必有希望2DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtifici
2、al IntelligenceSpring3.1 3.1 命题演算命题演算 u3.1.1 符号和命题命题演算的符号命题演算的符号：是命题符号：是命题符号,命题符号代表命题，是命题符号代表命题，是关于现实世界的能分辨真假值的陈述句。关于现实世界的能分辨真假值的陈述句。命题符号：命题符号：P，Q，R，S，T命题演算的符号：命题演算的符号：真值符号：真值符号：True,falseTrue,false 联结词：联结词：，=，通过联结词可把多个命题组成合成的命题，也称为通过联结词可把多个命题组成合成的命题，也称为合式公式。合式公式。3DepartmentofComputerScience&Technol
3、ogy,NanjingUniversityArtificial IntelligenceArtificial IntelligenceSpringu3.1.2 3.1.2 命题演算的语义命题演算的语义3.1 3.1 命题演算命题演算 如两个命题表达式如两个命题表达式在任何真值指派下都有相同的值，在任何真值指派下都有相同的值，则称为是等价的则称为是等价的（P29）表）表2.2所示的真值表证明：所示的真值表证明：P=Q与与PQ等价。等价。对于命题表达式对于命题表达式P，Q，R(P)=P;(PQ)(P=Q)4DepartmentofComputerScience&Technology,Nanjing
4、UniversityArtificial IntelligenceArtificial IntelligenceSpring否定律：否定律：(PQ)(PQ)(PQ)(PQ)分配律：分配律：P(QR)(PQ)(PR)分配律：分配律：P(QR)(PQ)(PR)交换律：交换律：(PQ)(QP)交换律：交换律：(PQ)(QP)结合律：结合律：(PQ)R)(P(QR)结合律：结合律：(PQ)R)(P(QR)置换律：置换律：(P=Q)(Q=P)3.1 3.1 命题演算命题演算 5DepartmentofComputerScience&Technology,NanjingUniversityArtifici
5、al IntelligenceArtificial IntelligenceSpring 3.2 3.2 谓词演算谓词演算命题演算中，命题演算中，P，Q代表一定的命题，如：代表一定的命题，如：P：星期四下雨：星期四下雨而谓词：而谓词：Weather（X，Y）代表日期与天气的关系）代表日期与天气的关系Weather（Tuesday，Rain）q 可以操纵命题演算表达式可以操纵命题演算表达式q允许包含变元允许包含变元Weather（X，Rain）6DepartmentofComputerScience&Technology,NanjingUniversityArtificial Intellige
6、nceArtificial IntelligenceSpring3.2.1谓词的语法和命题谓词的语法和命题 3.2 3.2 谓词演算谓词演算谓词演算的字母表组成：谓词演算的字母表组成：（1）英文字母组合，包括大写与小写）英文字母组合，包括大写与小写（2）数字集合）数字集合0,1,9（3）下划线）下划线如：如：Georgefiresbillxxxx7DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial IntelligenceSpring 谓词演算符号包括：谓词演算符号包
7、括：1.真值符号真值符号true和和false。2.常元符号常元符号,第一个字符为小写字母的符号表达式。第一个字符为小写字母的符号表达式。3.变元符号变元符号,第一个字符为大写字母的符号表达式。第一个字符为大写字母的符号表达式。4.函词符号函词符号,第一个字符为小写字母的符号表达式第一个字符为小写字母的符号表达式,函函词有一个元数词有一个元数,指出从定义域中映射到值域中的每个元指出从定义域中映射到值域中的每个元素。素。3.2 3.2 谓词演算谓词演算8DepartmentofComputerScience&Technology,NanjingUniversityArtificial Intel
8、ligenceArtificial IntelligenceSpring例：例：ulikes(george,kate).likes(X,george).u likes(george,susie).likes(X,X).u likes(george,sarah,tuesday).u friends(bill,richard).u friends(bill,george).u friends(father(david),father(andrew)u helps(bill,george).u helps(richard,bill).3.2 3.2 谓词演算谓词演算原子命题：是一个原子命题：是一个n
9、元谓词，后跟元谓词，后跟n个项，用括号括起来个项，用括号括起来并用逗号分开。并用逗号分开。谓词符号谓词符号常元符号常元符号项项9DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial IntelligenceSpring3.2.1谓词的语法和命题谓词的语法和命题u与谓词相关的一个正整数称为元数或与谓词相关的一个正整数称为元数或“参数数目参数数目”，具有相同的名但元数不同的谓词是不同的。具有相同的名但元数不同的谓词是不同的。u真值真值true和和false也是原子命题。也是
10、原子命题。u任何原子命题都能够用逻辑操作符将其变成谓词演算任何原子命题都能够用逻辑操作符将其变成谓词演算的命题。用的联结词也和命题演算一样的命题。用的联结词也和命题演算一样:,=和。和。u当一个变元在一个命题中作为参数出现时当一个变元在一个命题中作为参数出现时,它代表的它代表的是域中不特定的对象。谓词演算包括两个符号是域中不特定的对象。谓词演算包括两个符号,量词量词（全称量词）（全称量词）和彐（存在量词）和彐（存在量词）,用于限定包含变元用于限定包含变元的命题的含义。的命题的含义。10DepartmentofComputerScience&Technology,NanjingUniversit
11、yArtificial IntelligenceArtificial IntelligenceSpring3.2.1谓词的语法和命题谓词的语法和命题一个量词后面紧跟着一个变元和一个命题。例如：一个量词后面紧跟着一个变元和一个命题。例如：Xlikes(X,ice_cream).彐彐Yfriends(Y,peter).u全称量词全称量词,表明命题对于变元的变域中的所有的表明命题对于变元的变域中的所有的值都为真。值都为真。u存在量词彐存在量词彐,表明该命题对于变元的变域中的一些表明该命题对于变元的变域中的一些值为真。值为真。11DepartmentofComputerScience&Technolo
12、gy,NanjingUniversityArtificial IntelligenceArtificial IntelligenceSpring例：命题例：命题3.2.1谓词的语法和命题谓词的语法和命题plus(two,three)equal(plus(two,three)彐彐xfoo(x,two,plus(two,three)equal(plus(two,three),five)12DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial IntelligenceSpri
13、ng3.2.2谓词演算的语义谓词演算的语义谓词演算的语义提供了确定合式表达式真值的形式基础。谓词演算的语义提供了确定合式表达式真值的形式基础。表达式的真值依赖于常元、变元、谓词、函词到论域表达式的真值依赖于常元、变元、谓词、函词到论域中的映射，在论域中的关系的真假决定了相应表达式中的映射，在论域中的关系的真假决定了相应表达式的真假。的真假。例如：例如：ufriends(george,susie)ufriends(george,kate)13DepartmentofComputerScience&Technology,NanjingUniversityArtificial Intelligenc
14、eArtificial IntelligenceSpring3.2.2谓词演算的语义谓词演算的语义一个论域一个论域D上的解释：上的解释：假设论域假设论域D是一个非空集合，在是一个非空集合，在D上的一个解释把论域上的一个解释把论域D的的实体指派给一个谓词演算表达式的每一个常元、变元、谓词实体指派给一个谓词演算表达式的每一个常元、变元、谓词及函词符号，于是有：及函词符号，于是有：1）每一个常元指派了）每一个常元指派了D的一个元素。的一个元素。2）对每一个变元，指派）对每一个变元，指派D的一个非空集合，这是该变元的的一个非空集合，这是该变元的变域。变域。3）每个）每个n元谓词元谓词P定义在论域定义在
15、论域D中的中的n个参数上，并定义了从个参数上，并定义了从Dn到到T，F的一个映射。的一个映射。4)每个每个m元函词元函词f定义在论域定义在论域D的的m个参数上，并定义了从个参数上，并定义了从Dm到到T，F的一个映射。的一个映射。在一种解释下，一个表达式的意义是在该解释下的一个真值在一种解释下，一个表达式的意义是在该解释下的一个真值指派。指派。14DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial IntelligenceSpring3.2.2谓词演算的语义谓词演算的语
16、义谓词演算表达式的真值谓词演算表达式的真值设有表达式设有表达式E和在非空论域和在非空论域D上对上对E的一个解释的一个解释I，E的真值的真值按以下规律决定：按以下规律决定：1）一个常元的值是根据）一个常元的值是根据I指派给它的指派给它的D的一个元素。的一个元素。2）一个变元的值是根据）一个变元的值是根据I指派给它的指派给它的D的一个元素集合。的一个元素集合。3）一个函词的值是根据由）一个函词的值是根据由I指派给它的参数值计算得到的指派给它的参数值计算得到的D的元素。的元素。4）真值符号）真值符号true的值是的值是T，false的值是的值是F。5）原子命题的值或者为）原子命题的值或者为T，或者为
17、，或者为F，取决于解释，取决于解释I。6）如果一个命题的值为）如果一个命题的值为F，则其否定式为，则其否定式为T，否则为，否则为F。7）如果）如果11)如果对于在解释如果对于在解释I下的下的X的每一个指派，的每一个指派，S的值为的值为T，则，则 XS为为T，否则为，否则为F。12）如果在解释）如果在解释I下存在下存在X的一个指派使得的一个指派使得S的值为的值为T，则，则彐彐XS为为T，否则为，否则为F。15DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial Intel
18、ligenceSpring3.2.2谓词演算的语义谓词演算的语义变元：变元：likes(george,X)这个变元名可以由任何其他变元名代替，不会改变表这个变元名可以由任何其他变元名代替，不会改变表达式的意思。达式的意思。l变元的量词约束是谓词演算语义的重要部分变元的量词约束是谓词演算语义的重要部分 在谓词演算中在谓词演算中,变元有两种约束使用的方法变元有两种约束使用的方法:q在特定解释下在特定解释下,命题对变元的变域中的所有常元指派命题对变元的变域中的所有常元指派为真为真,则称该变元是则称该变元是全称性变元全称性变元。代表全称量词的符号。代表全称量词的符号是是 ,括号常常用于表示量词的约束范
19、围括号常常用于表示量词的约束范围 q存在性变元存在性变元。至少存在变元的变域中的一个值使包含。至少存在变元的变域中的一个值使包含变元的表达式为真时，表达式才为真。变元的表达式为真时，表达式才为真。代表存在量词的代表存在量词的符号是彐符号是彐16DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial IntelligenceSpring3.2.2谓词演算的语义谓词演算的语义否定与全称量词、存在量词之间的关系否定与全称量词、存在量词之间的关系。对于谓词对于谓词P,Q,变元变元
20、X,Y有：有：u彐彐XP(X)XP(X)u XP(X)彐彐XP(X)u彐彐XP(X)彐彐YP(Y)u XQ(X)YQ(Y)u X(P(X)Q(X)XP(X)YQ(Y)u彐彐X(P(X)Q(X)彐彐XP(X)彐彐YQ(Y)17DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial IntelligenceSpring3.3 3.3 推理规则产生谓词演算表达式推理规则产生谓词演算表达式 3.3.1推理规则推理规则推理规则：实际上是一个从其他谓词演算命题产生新的谓推理规则：实际
21、上是一个从其他谓词演算命题产生新的谓词演算命题的机械方法。亦即推理规则产生基于给定逻词演算命题的机械方法。亦即推理规则产生基于给定逻辑断言的句法形式的新命题。当每个由逻辑表达式集辑断言的句法形式的新命题。当每个由逻辑表达式集S上的推理规则产生的命题上的推理规则产生的命题X都是都是S的逻辑结果的逻辑结果,则称该逻则称该逻辑规则是合理的。辑规则是合理的。S:Xhuman(X)=mortal(X).human(Socrates).X:mortal(Socrates).18DepartmentofComputerScience&Technology,NanjingUniversityArtificia
22、l IntelligenceArtificial IntelligenceSpring假言推理和消解原理都是合理的推理规则的例子。假言推理和消解原理都是合理的推理规则的例子。假言推理：如果命题假言推理：如果命题P，P=Q为真，应用假言推理得为真，应用假言推理得出出Q为真。为真。S:Xhuman(X)=mortal(X).human(Socrates).X:mortal(Socrates).human(Socrates)=mortal(Socrates)？human(X)Socrates合一合一算法算法19DepartmentofComputerScience&Technology,Nanjin
23、gUniversityArtificial IntelligenceArtificial IntelligenceSpring3.3.2合一合一u伪代码写的函数伪代码写的函数Unify用于计算两个谓词表达式的最一般合一用于计算两个谓词表达式的最一般合一q是判断两个谓词表达式匹配所需的一种代入算法是判断两个谓词表达式匹配所需的一种代入算法q合一表明了两个或多个表达式在什么条件下可以称合一表明了两个或多个表达式在什么条件下可以称为等价的。为等价的。以两个谓词演算表达式为参数以两个谓词演算表达式为参数,若这两个表达式可以合若这两个表达式可以合一一,则返回则返回最一般合一代入最一般合一代入,否则返回否
24、则返回FAIL。20DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial IntelligenceSpring3.3.2合一合一functionunify(E1,E2);begincaseend%endcaseendq首先首先,它递归地试图对表达式的初始成分合一。如果成它递归地试图对表达式的初始成分合一。如果成功功,这次合一返回的任何代入式被用到两个表达式的剩这次合一返回的任何代入式被用到两个表达式的剩下部分下部分,然后以这两个表达式为参数。然后以这两个表达式为参数。q
25、终止条件是两个参数之一为一个符号终止条件是两个参数之一为一个符号(谓词名谓词名,函词函词名名,变元变元,常元常元),或两个表达式的每一元素都已匹配了。或两个表达式的每一元素都已匹配了。21DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial IntelligenceSpring3.3.2合一合一caseE1,E2或者是常元或者是空表或者是常元或者是空表:%递归终止。递归终止。IfE1E2thenreturnelsereturnFAIL;E1是一个变元是一个变元:ifE1
26、在在E2中出现中出现thenreturnFAILelsereturnE2/E1;E2是一个变元是一个变元:ifE2在在E1中出现中出现thenreturnFAILelsereturnE1/E2;其他情况其他情况:%E1和和E2都是表都是表22DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial IntelligenceSpring3.3.2合一合一beginHE1:=E1的第一个元素的第一个元素;HE2:=E2的第一个元素的第一个元素;SUBS1:=unify(HE1,
27、HE2);ifSUBS1FAILthenreturnFAILTE1:=apply(SUBS1,E1的后半部的后半部)TE2:=apply(SUBS1,E2的后半部的后半部)SUBS2:=unify(TE1,TE2),ifSUBS2FAILthenreturnFAILelsereturnSUBS1与与SUBS2的合成的合成end23DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial IntelligenceSpring3.3.3合一的一个例子合一的一个例子通过以下调用来
28、跟踪算法的运行过程：通过以下调用来跟踪算法的运行过程：unify(parentsX(fatherX)(motherbill),(parentsbill(fatherbill)Y)第一次调用第一次调用:unify(parents,parents)这次调用成功这次调用成功,返回代入集返回代入集。第二次调用第二次调用:unify(X,bill)这次调用成功这次调用成功,返回代入返回代入bill/X。24DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial Intelligen
29、ceSpring3.3.3合一的一个例子合一的一个例子在此基础上又调用在此基础上又调用:unify(fatherbill)(motherbill),(fatherbill)Y)导致调用导致调用:(1)unify(fatherbill),(fatherbill)unify(father,father)unify(bill,bill)unify(),()所有的调用都成功所有的调用都成功,返回空代入集返回空代入集。(2)unify(motherbill),Y)bill/X,(motherbill)/Y25DepartmentofComputerScience&Technology,NanjingUn
30、iversityArtificial IntelligenceArtificial IntelligenceSpring3.4 3.4 应用应用 :一个基于逻辑的金融投资辅助决策程序一位有三个人需赡养一位有三个人需赡养,有有$22000存款存款,每年有每年有$25000的稳定收入的的稳定收入的投资者的情况投资者的情况,可产生一个由下列命题组成的逻辑系统可产生一个由下列命题组成的逻辑系统:1.savings(inadequate)=investment(savings).2.savings(adequate)income(adequate)=investment(stocks).3.Saving
31、s(adequate)income(inadequate)=investment(combination).4.Xamountsaved(X)彐彐Y(dependents(Y)greater(X,minsavings(Y)=savings(adequate).5.Xamountsaved(X)彐彐Y(dependents(Y)greater(X,minsavings(Y)=savings(inadequate).26DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial
32、IntelligenceSpring3.4应用应用6.Xearnings(X,steady)彐彐Y(dependents(Y)greater(X,minincome(Y)=income(adequate).7.Xearnings(X,steady)彐彐Y(dependents(Y)greater(X,minincome(Y)=income(inadequate).8.Xearnings(X,unsteady)=income(inadequate).9.amountsaved(22000).10.earnings(25000,steady).11.dependents(3).其中:minsavi
33、ngs(X)=5000*X;minincome(X)=15000+(4000*X)27DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial IntelligenceSpring3.4应用应用u第一步把第第一步把第10、11与第与第7的前提合一的前提合一,得得:12.Income(inadequate).u第二步把第第二步把第9、11与第与第4的前提合一的前提合一,得得:13.savings(adequate)将第将第12、13条命题检验第条命题检验第3条命题得到其前提为
34、真。于条命题得到其前提为真。于是运用假言推理后得到结论是运用假言推理后得到结论:investment(combination),这就是给投资者的建议。这就是给投资者的建议。(存款的人应该把他们多余的钱分别用于存款和买股票，在增加存款存款的人应该把他们多余的钱分别用于存款和买股票，在增加存款做保险的同时试图通过做股票以增加收入。做保险的同时试图通过做股票以增加收入。)28DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial IntelligenceSpring3.5 3.
35、5 消解定理证明消解定理证明 u消解是一种应用于谓词演算中的定理证明技术，是人工智能问题求解的消解是一种应用于谓词演算中的定理证明技术，是人工智能问题求解的一个组成部分。消解描述了如何用最少的合一次数在一个子句数据库中一个组成部分。消解描述了如何用最少的合一次数在一个子句数据库中发现矛盾的方法。发现矛盾的方法。u具体方法如下：具体方法如下：对所要证明的命题取反，把它加到已知为真的公理集中，然后用消解推对所要证明的命题取反，把它加到已知为真的公理集中，然后用消解推理规则证明这将导致一个矛盾，一旦证明了否定目标与已知公理集不一理规则证明这将导致一个矛盾，一旦证明了否定目标与已知公理集不一致，就能推
36、导出原来的目标与已知公理集是一致的，从而定理得证。致，就能推导出原来的目标与已知公理集是一致的，从而定理得证。29DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial IntelligenceSpring3.5消解定理证明消解定理证明3.5.1引言引言消解否证包含以下步骤：消解否证包含以下步骤：u把前提或公理转换成子句形式。把前提或公理转换成子句形式。u把求证目标的否定的子句形式加到公理集合中。把求证目标的否定的子句形式加到公理集合中。u对所有这些子句进行消解，产生它们
37、的逻辑结果子句。对所有这些子句进行消解，产生它们的逻辑结果子句。u用产生空子句的方法来得出矛盾。用产生空子句的方法来得出矛盾。u否定目标的否证在用于产生空子句的代换下为真。否定目标的否证在用于产生空子句的代换下为真。30DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial IntelligenceSpring3.5.1引言引言u消解否证需要所有公理和否定目标为子句形式消解否证需要所有公理和否定目标为子句形式子句形式把一个逻辑数据库子句形式把一个逻辑数据库表示为一个文字析
38、取式的集表示为一个文字析取式的集合。一个文字是一个原子表合。一个文字是一个原子表达式或原子表达式的否定。达式或原子表达式的否定。u消解作用于两个子句消解作用于两个子句,其中一个包含某文字其中一个包含某文字,另一另一个包含该文字的否定个包含该文字的否定,如果这些文字包含变元如果这些文字包含变元,必须用必须用合一使它们相等。合一使它们相等。u一个新的子句就此产生了一个新的子句就此产生了,它包含两个子句中所有它包含两个子句中所有谓词的谓词的析取析取,除了该文字和它的否定以外。除了该文字和它的否定以外。31DepartmentofComputerScience&Technology,NanjingUn
39、iversityArtificial IntelligenceArtificial IntelligenceSpring3.5.1引言引言用消解所做的等价的推理把以下谓词演算公式变换成子句形式用消解所做的等价的推理把以下谓词演算公式变换成子句形式：谓词形式谓词形式子句形式子句形式1.Alldogsareanimals(X)(dog(X)animal(X)dog(X)animal(X)2.Fidoisadogdog(fido)dog(fido)3.allanimalswilldie(Y)(animal(Y)die(Y)animal(Y)die(Y)证明：证明：fidowilldie对目标对目标“
40、取反取反”：die(fido)32DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial IntelligenceSpringdog(X)animal(X).animal(Y)die(Y).Y/Xdog(fido).dog(Y)die(Y).fido/Ydie(fido).die(fido).图图“死狗死狗”问题消解证明问题消解证明3.5.1引言引言33DepartmentofComputerScience&Technology,NanjingUniversityArti
41、ficial IntelligenceArtificial IntelligenceSpring3.5.2为消解否证产生子句形式为消解否证产生子句形式u本节提出一个由一系列变换组成的算法，这些变换可本节提出一个由一系列变换组成的算法，这些变换可以把任何谓词演算表达式归约为子句形式，在此过程以把任何谓词演算表达式归约为子句形式，在此过程中中保持其真值、一般性和不可满足性不变保持其真值、一般性和不可满足性不变。即如果在原谓词演算表达式中即如果在原谓词演算表达式中存在一个矛盾，则其子句形式存在一个矛盾，则其子句形式中也存在一个矛盾，变换不牺中也存在一个矛盾，变换不牺牲消解否证的完备性。牲消解否证的完
42、备性。34DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial IntelligenceSpring3.5.2为消解否证产生子句形式为消解否证产生子句形式设设X,Y,Z,W表示变元；表示变元；l,m,n表示常元；表示常元；a,b,c,d,e表示谓词名。表示谓词名。要归纳为子句的表达式：要归纳为子句的表达式：1.(X)(a(X)b(X)c(X,l)(彐彐Y)(彐彐Z)c(Y，Z)d(X,Y)(X)(e(X)2.(X)(a(X)b(X)c(X，l)(彐彐y)(彐彐Z)c(Y
43、,Z)d(X,Y)(）(e(X)）3.(X)(a(X)b(X)c(X,l)(彐彐Y)(Z)c(Y,Z)d(X,Y)(X)(e(X)4.(X)(a(X)b(X)c(X,l)(彐彐Y)(Z)c(Y,Z)d(X,Y)(W)(e(W)所有量词移到最左边而不改变其次序所有量词移到最左边而不改变其次序5.(X)(彐彐Y)(Z)(W)(a(X)b(X)c(X,l)c(Y,Z)d(X,Y)e(W)前束范式前束范式斯柯伦标准化去掉所有的存在量词斯柯伦标准化去掉所有的存在量词35DepartmentofComputerScience&Technology,NanjingUniversityArtificial I
44、ntelligenceArtificial IntelligenceSpring3.5.2为消解否证产生子句形式为消解否证产生子句形式斯柯伦标准化：去掉所有的存在量词斯柯伦标准化：去掉所有的存在量词彐彐Z（foo(Y，Z)foo(Y，k)彐彐X（dog(X)dog(fido)斯柯伦常元斯柯伦常元如果谓词中含有多个参数，而如果谓词中含有多个参数，而彐约束变元在彐约束变元在 约束变约束变元的约束范围内，元的约束范围内，则彐约束变元必须是那些其他变元则彐约束变元必须是那些其他变元的函数。的函数。如：如：（X）(彐彐Y)(mother(X,Y)（X）(mother(X,m(X)36Department
45、ofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial IntelligenceSpring3.5.2为消解否证产生子句形式为消解否证产生子句形式6.(X)(Z)(W)(a(X)b(X)c(X,l)c(f(X),Z)d(X,f(X)e(W)5.(X)(彐彐Y)(Z)(W)(a(X)b(X)c(X,l)c(Y,Z)d(X,Y)e(W)斯柯伦标准化后斯柯伦标准化后去掉全称量词去掉全称量词7.(a(X)b(X)c(X,l)(c(f(X),Z)d(X,f(X)e(W)8.a(X)b(X)c(X,l)
46、e(W)a(X)b(X)c(f(X),Z)d(X,f(X)e(W)转换成析取式的合取转换成析取式的合取每个合取式为一个分离的子句每个合取式为一个分离的子句9a:a(X)b(X)c(X,l)e(W)9b:a(X)b(X)c(f(X),Z)d(X,f(X)e(W)把分离的变元归一化把分离的变元归一化10a:a(X)b(X)c(X,l)e(W)10b:a(U)b(U)c(f(U),Z)d(U,f(U)e(V)37DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial Intel
47、ligenceSpring3.5.3消解证明过程消解证明过程u例例1:“幸运学生幸运学生”的故事的故事:“任何通过了历史考试并中了彩票的人是快乐的。任何通过了历史考试并中了彩票的人是快乐的。任何肯学习或幸运的人可以通过所有考试任何肯学习或幸运的人可以通过所有考试,John不不学习但很幸运学习但很幸运,任何人只要是幸运的就能中彩。任何人只要是幸运的就能中彩。John快乐吗快乐吗?1.第一步把这些句子变成谓词形式第一步把这些句子变成谓词形式:定义一些函词：定义一些函词：pass(x,y),win(x,lottery),happy(x),study(X),lucky(x)38Departmentof
48、ComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial IntelligenceSpring3.5.3 3.5.3 消解证明过程消解证明过程“任何通过了历史考试并中了彩票的人是快乐的。任何肯学习或任何通过了历史考试并中了彩票的人是快乐的。任何肯学习或幸运的人可以通过所有考试幸运的人可以通过所有考试,John不学习但很幸运不学习但很幸运,任何人只要任何人只要是幸运的就能中彩。是幸运的就能中彩。John快乐吗快乐吗?X(pass(X,history)win(X,lottery)happy(X)X Y
49、(study(X)lucky(X)pass(X,Y)study(john)lucky(john)X(lucky(X)win(X,lottery)39DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtificial IntelligenceSpring3.5.3消解证明过程消解证明过程1.pass(X,history)win(X,lottery)happy(X)2.study(Y)pass(Y,Z)3.lucky(V)pass(V,W)4.study(john)5.lucky(joh
50、n)6.lucky(U)win(U,lottery)X(pass(X,history)win(X,lottery)happy(X)X Y(study(X)lucky(X)pass(X,Y)study(john)lucky(john)X(lucky(X)win(X,lottery)将这四个谓词演算命题转换成子句形式将这四个谓词演算命题转换成子句形式:加入子句形式的否定目标加入子句形式的否定目标:7.happy(john)40DepartmentofComputerScience&Technology,NanjingUniversityArtificial IntelligenceArtifici