《所有分类基于谓词逻辑的机器推理.pptx》由会员分享，可在线阅读，更多相关《所有分类基于谓词逻辑的机器推理.pptx（171页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。
1、2023/3/241目录5.0 机器推理概述5.1 一阶谓词逻辑5.2 归结演绎推理5.3 应用归结原理求取问题答案5.4 归结策略5.5 归结反演程序举例*5.6 Horn子句归结与逻辑程序5.7 非归结演绎推理第1页/共171页2023/3/2425.0 机器推理概述（1）n机器推理：就是计算机推理，也称自动推理。它是人工智能的核心课题之一。推理是人脑的一个基本功能和重要功能。几乎所有的人工智能领域都与推理有关。因此，要实现人工智能，就必须将推理的功能赋予机器，实现机器推理。n自动定理证明：是机器推理的一种重要应用，它是利用计算机证明非数值性的结果，很多非数值领域的任务如医疗诊断、信息检索
2、、规划制定和难题求解等方法都可以转化一个定理证明问题。第2页/共171页2023/3/243n自动定理证明的基本方法：5.0 机器推理概述（2）定理证明器：它是研究一切可判定问题的证明方法。鲁滨逊的归结原理。人机交互进行定理证明：计算机作为数学家的辅助工具，用计算机帮助人完成手工证明中的难以完成的烦杂的大量计算推理和穷举。典型代表：四色定理的证明。判定法：该方法是对一类问题找出统一的计算机上可实现的算法。典型代表：数学家吴文俊教授吴氏方法。自然演绎法：该方法依据推理规则从前提和公理中可以推出许多定理，如果待证明的定理在其中则定理得证。典型代表：LT程序、证明平面几何的程序。第3页/共171页2
3、023/3/244n基于归结原理的自动定理证明过程：5.0 机器推理概述（3）定理的自然语言描述定理的谓词公式描述子句集生成子句集定理得证应用归结规则归结策略自然语言处理生成谓词公式已知前提：F1：自然数都是大于零的整数。F2：所有整数不是偶数就是奇数。F3：偶数除以2是整数。结论G：所有自然数不是奇数就是除以2为整数的数。定理的谓词公式描述：F1:x(N(x)GZ(x)I(x)F2:x(I(x)(E(x)O(x)F3:x(E(x)I(s(x)G:x(N(x)(I(s(x)O(x)第4页/共171页2023/3/2455.1 5.1 一阶谓词逻辑5.1.1 谓词、函数、量词5.1.2 谓词公式
4、5.1.3 谓词逻辑中的形式演绎推理第5页/共171页2023/3/2465.1.1 谓词、函数、量词（1）命题（proposition）：是具有真假意义的语句。命题代表人们进行思维时的一种判断，或者是否定，或者是肯定。命题可以用命题符号表示，如：用命题符号可以表示简单的逻辑关系和推理。P:今天天气好 Q:去旅游S1：我有名字 S2：你有名字PQ：表示如果今天天气好，就去旅游。此时，如果P（今天天气好）成立，则可以得到结论Q（去旅游）第6页/共171页2023/3/2475.1.1 5.1.1 谓词、函数、量词（2 2）对于复杂的知识，命题符号能力不够。无法把所描述的客观事物的结构及逻辑特征反
5、映出来。无法把不同事物间的共同特征表达出来。F：老李是小李的父亲。S1：我有名字 S2：你有名字所有的人都有名字：S1S2 S3 第7页/共171页2023/3/2485.1.15.1.1谓词、函数、量词（3 3）谓词(predicate)：一般形式为P(x1,x2,xn)其中，P为谓词名，用于刻画个体的性质、状态或个体间的关系。x1,x2,xn是个体，表示某个独立存在的事物或者某个抽象的概念。例如：S(x):x是学生；P(x,y):x是y的双亲。个体变元的变化范围称为个体域。包揽一切事物的集合称为全总个体域。第8页/共171页2023/3/2495.1.1 5.1.1 谓词、函数、量词（4
6、4）函数：为了表达个体之间的对应关系，引入数学中函数概念和记法。用形如f(x1,x2,xn)来表示个体变元对应的个体y，并称之为n元个体函数，简称函数。f是函数符号。函数增强了谓词的表达能力函数father(x):值为x的父亲。谓词Doctor(father(Li):表示Li的父亲是医生，值为真或假。符号约定：谓词符号大写字母；P(x,y)函数符号小写字母；f(x)个体变元符号 x、y、z、u、v 个体常元符号 a、b、c.。P(a,b)第9页/共171页2023/3/2410逻辑联结词联结词联结词优先级优先级应用应用否定否定1p,非非p合取合取2p q,不仅不仅p,而且而且q、既、既p,又又
7、q、一边、一边p,一边一边q、虽然虽然p,但是但是q 析取析取2相容的或相容的或p q,排斥的或排斥的或p q p q 蕴含蕴含3p-q，q是是p的必要条件，的必要条件，p是是q的充分条件。的充分条件。只要只要p就就q、p仅当仅当q、只有、只有q才才p 等价等价3p q，p和和q互为充分必要条件互为充分必要条件P当且仅当当且仅当q同级从左向右顺序演算第10页/共171页2023/3/24115.1.1 5.1.1 谓词、函数、量词（5 5）表示“对个体域中所有的（或任一个）个体”。记为x所有、一切、全体、凡是等词统称为全称量词全称量词：表示“在个体域中存在个体”。记为x存在、有些、有的、至少有
8、一个等词统称为存在量词存在量词：如：“凡是人都有名字”用M（x）表示“x是人”，N（x）表示“x有名字”x（M（x）N（x）如：“存在不是偶数的整数”用G（x）表示“x是整数”，E（x）表示“x是偶数”x（G（x）E（x）第11页/共171页2023/3/24125.1.1 5.1.1 谓词、函数、量词（6 6）用谓词表示命题时，一般取全总个体域，再采用使用限定谓词的方法来指出每个个体变元的个体域。(2)对存在量词，把限定词作为一个合取项加入。即 x(P(x)例5.2：对于所有的自然数，均有x+yx x y（N（x）N（y）S(x,y,x)）例5.3：某些人对某些食物过敏 x y(M(x)N(
9、y)G(x,y)(1)对全称量词，把限定词作为蕴含式之前件加入。即 x（P（x）例5.2：对于所有的自然数，均有x+yx 也可以用函数h（x，y）来表示x与y的和 x y（N（x）N（y）G(h(x,y),x)）第12页/共171页2023/3/24135.1.1 5.1.1 谓词、函数、量词（7 7）例5.1：不存在最大的整数，我们可以把它表示为：x(G(x)y(G(y)D(x，y)x(G(x)y(G(y)D(y，x)用谓词表示命题时，形式并不是固定的。第13页/共171页2023/3/24145.1.15.1.1谓词、函数、量词（8 8）练习：用谓词公式表示下述命题。已知前提：（1）自然数
10、都是大于零的整数。（2）所有整数不是偶数就是奇数。（3）偶数除以2是整数。结论：所有自然数不是奇数就是除以2为整数的数。首先定义如下谓词：N(x):x是自然数。I(x):x是整数。E(x):x是偶数。O(x):x是奇数。GZ(x):x大于零。s(x):x除以2。第14页/共171页2023/3/24155.1.1 5.1.1 谓词、函数、量词（9 9）将上述各语句翻译成谓词公式：（1）自然数都是大于零的整数。F1:x(N(x)GZ(x)I(x)（2）所有整数不是偶数就是奇数。F2:x(I(x)(E(x)O(x)（3）偶数除以2是整数。F3:x(E(x)I(s(x)所有自然数不是奇数就是除以2为
11、整数的数。G:x(N(x)(I(s(x)O(x)第15页/共171页2023/3/24165.1.2 5.1.2 谓词公式（1 1）定义1：项（1）个体常元和变元都是项。（2）f是n元函数符号，若t1，t2，tn是项，则 f(t1，t2，tn)是项。（3）只有有限次使用（1），（2）得到的符号串才是项。用谓词、量词及真值连结词可以表达相当复杂的命题，我们把命题的这种符号表达式称为谓词公式。第16页/共171页2023/3/24175.1.2 5.1.2 谓词公式（2 2）定义2：原子公式设P为n元谓词符号，t1，t2，tn为项，P(t1，t2，tn)称为原子谓词公式，简称原子或原子公式。从原子
12、谓词公式出发，通过命题联结词和量词，可以组成复合谓词公式。第17页/共171页2023/3/24185.1.2 5.1.2 谓词公式（3 3）定义3：谓词公式（1）原子公式是谓词公式。（2）若A、B是谓词公式，则A，A B，A B，A B，AB，xA，xA也是谓词公式。（3）只有有限步应用（1）（2）生成的公式才是谓词公式。谓词公式亦称为谓词逻辑中的合适（式）公式，记为Wff。由项的定义，当t1，t2，tn全为个体常元时，所得的原子谓词公式就是原子命题公式（命题符号）。所以全体命题公式也是谓词公式。第18页/共171页2023/3/24195.1.2 5.1.2 谓词公式（4 4）辖域：紧接于
13、量词之后被量词作用（即说明）的谓词公式称为该量词的辖域。指导变元：量词后的变元为指导变元。约束变元：在一个量词辖域中与该量词的指导变元相同的变元称为约束变元。自由变元：谓词公式中除了约束变元之外的变元。（1）x P(x)（2）y(G(y)D(x,y)（3）x G(x)P(x)指导变元约束变元约束变元约束变元自由变元自由变元第19页/共171页2023/3/24205.1.2 5.1.2 谓词公式（5 5）一个变元在一个公式中既可以约束出现，也可以自由出现，为了避免混淆，通过改名规则改名：对需要改名的变元，应同时更改该变元在量词及其辖域中的所有出现。新变元符号必须是量词辖域内原先没有的，最好是公
14、式中也未出现过的。xG(x)P(x)改为xG(x)P(y)或yG(y)P(x)第20页/共171页2023/3/24215.1.2 5.1.2 谓词公式（6 6）谓词公式与命题的区别与联系谓词公式是命题函数。一个谓词公式中所有个体变元被量化（在谓词前加上量词），谓词公式就变成了一个命题。从谓词公式得到命题的两种方法：给谓词中的个体变元代入个体常元；把谓词中的个体变元全部量化。例：谓词公式P（x）表示“x是素数”P（a）x P（x）,x P（x）都是命题第21页/共171页2023/3/24225.1.2 5.1.2 谓词公式（7 7）一阶谓词：仅个体变元被量化的谓词。二阶谓词：不仅个体变元被量
15、化，函数符号和谓词符号也被量化。如：P x P（x）以下两种命题在个体域为有限集时（n个元素），有下面的等价式全称命题：xP(x)等价于P(a1)P(a2)P(an)特称命题 xG(x)等价于P(a1)P(a2)P(an)第22页/共171页2023/3/24235.1.2 5.1.2 谓词公式（8 8）定义4：合取范式（Conjunctive Normal Form）设A为如下形式的谓词公式：B1B2 Bn其中Bi（i=1,2,，n）形如L1 L2 Lm，Lj（j=1，2,，m）为原子公式或其否定，则A称为合取范式。例(P(x)Q(y)(P(x)Q(y)R(x,y)(Q(x)R(x,y)就是
16、一个合取范式应用逻辑等价式，任一谓词公式可化为与之等价的合取范式，一个谓词的合取范式不唯一第23页/共171页2023/3/24245.1.2 5.1.2 谓词公式（9 9）定义5：析取范式（Disjunctive Normal Form）设A为如下形式的谓词公式：B1 B2 Bn其中Bi（i=1,2,，n）形如L1 L2 Lm，Lj（j=1，2,，m）为原子公式或其否定，则A称为析取范式。例(P(x)Q(y)R(x,y)(P(x)Q(y)(P(x)R(x,y)就是一个析取范式应用逻辑等价式，任一谓词公式可化为与之等价的析取范式，一个谓词的析取范式不唯一第24页/共171页2023/3/242
17、55.1.2 5.1.2 谓词公式（1010）*谓词公式的解释：对谓词公式中的各种变量指定特殊的常量去替代。设D为谓词公式P的个体域，若对P中的个体常量、函数和谓词按如下规定赋值：（1）为每个个体常量指派D中的一个元素；（2）为每个n元函数指派一个从Dn到D的映射，其中 Dn(x1,x2,xn)|x1,x2,xn D （3）为每个n元谓词指派一个从Dn到F,T的映射。称这些指派(谓词公式的解释)为公式P在D上的一个解释。当被解释的谓词公式在特定解释下真值为真，称这个解释满足这个谓词公式。第25页/共171页2023/3/2426谓词公式的解释*用某个解释解释一个谓词公式，就是将解释中的各个值带
18、到谓词公式中去，要全部取到。约束出现的变元取值关系与量词性质有关，当指导变元的相应量词为存在量词，此时每个个体域的取值所对应的谓词真值的关系为或关系，也就是说在个体域中有一个特定点解释该谓词公式即可。当指导变元的相应量词为全称量词，此时每个个体与的取值所对应的谓词真值的关系为与关系，也就是说在个体域中所有的特定点同时解释该谓词公式。第26页/共171页2023/3/24275.1.2 5.1.2 谓词公式（1111）*例：设个体域D1,2,求公式AxyP(x，y)在D上的解释，并指出在每一种解释下公式A的真值。解：公式里没有个体常量和函数，所以直接为谓词指派真值，设为 P（1，1）T P（1，
19、2）F P（2，1）T P（2，2）F 这就是A在D上的一个解释。在此解释下：当x1时有y1使P（x，y）的真值为T；当x2时有y1使P（x，y）的真值为T；即对于D中的所有X都有y1使P（x，y）的真值为T，所以在此解释下公式A的真值为T。第27页/共171页2023/3/2428补充前题设个体域D1,2,求公式AxyP(x，y)在D上的解释，并指出在每一种解释下公式A的真值。xyP(x，y)=(P(1,1)P(1,2)(P(2,1)P(2,2)取P(1,1)=T,P(1,2)=T,P(2,1)=F,P(2,2)=F 时,A的真值为F。取P(1,1)=T,P(1,2)=F,P(2,1)=F,
20、P(2,2)=T 时,A的真值为T。第28页/共171页5.1.2 5.1.2 谓词公式（1212）*例：设个体域D1,2,求公式BxP（x）Q（f(x),b）在D上的解释，并指出在每一种解释下公式B的真值。解：为个体常量b指派D中的值：b=1 为函数f(x)指派D中的值:f(1)=2,f(2)=1 对谓词指派真值为：P(1)=F,P(2)=T,Q(1,1)=T,Q(2,1)=F 在此解释下，当x1时：P(1)=F,Q(f(1),1)=Q(2,1)=F 所以P（x）Q（f(x),b）为T。当x2时有:P(2)=T,Q(f(2),1)=Q(1,1)=T 所以P（x）Q（f(x),b）为T。即对个
21、体域D中的所有x均有P（x）Q（f(x),b），所以公式B在此解释下的真值为T。第29页/共171页2023/3/24305.1.2 5.1.2 谓词公式（1414）定义6：谓词公式在个体域上的永真、永假、可满足设P为谓词公式，D为其个体域，对于D中的任一解释I：（1）若P恒为真，则称P在D上永真或是D上的永真式。（2）若P恒为假，则称P在D上永假或是D上的永假式。（3）若至少有一个解释，可使P为真，则称P在D上是可满足式。第30页/共171页2023/3/24315.1.2 5.1.2 谓词公式（1515）定义7：谓词公式全个体域上的永真、永假、可满足设P为谓词公式，对于任何个体域：（1）若
22、P都永真，则称P为永真式。（2）若P都永假，则称P为永假式。（3）若P都可满足，则称P为可满足式。谓词公式的真值与个体域及解释有关，考虑到个体域的数目和个体域中元素数目无限的情形，所以要通过算法判断一个谓词公式永真是不可能的，所以称一阶谓词逻辑是不可判定的（半可判定）。第31页/共171页2023/3/24325.1.3 5.1.3 谓词逻辑中的形式演绎推理（1 1）自然演绎推理 利用一阶谓词推理规则的符号表示形式，可以把关于自然语言的逻辑推理问题，转化为符号表达式的推演变换。这种推理十分类似于人们用自然语言推理的思维过程，因而称为自然演绎推理。在推理过程中常用到的推理规则的符号表示形式：常用
23、逻辑等价式常用逻辑蕴含式 第32页/共171页2023/3/2433常用逻辑等价式（1 1）第33页/共171页2023/3/2434常用逻辑等价式（2 2）第34页/共171页2023/3/2435常用逻辑等价式（3 3）第35页/共171页2023/3/2436常用逻辑等价式（4 4）第36页/共171页2023/3/2437常用逻辑蕴含式（1)1)第37页/共171页2023/3/2438常用逻辑蕴含式(2)(2)第38页/共171页2023/3/24395.1.3 5.1.3 谓词逻辑中的形式演绎推理（2 2）例5.4 设有前提：（1）凡是大学生都学过计算机；（2）小王是大学生。试问：
24、小王学过计算机吗？解：令S（x）：x是大学生M（x）：x学过计算机；a：小王上面命题用谓词公式表示为：前提(1),US前提(2),(3),I3我们进行形式推理：M(a)，即小王学过计算机。xA(x)=A(y)y是个体域中任一确定元素(A B)A=B,假言推理第39页/共171页2023/3/24405.1.3 5.1.3 谓词逻辑中的形式演绎推理（3 3）例5.5 证明 是 和 的逻辑 结果。证：前提(1),US(2),US前提(3),(4),I4(A B)B=A 拒取式得证第40页/共171页2023/3/24415.1.3 5.1.3 谓词逻辑中的形式演绎推理（4 4）例5.6 证明 证：
25、前提(1),US(2),E24(3),(5),I6前提(4),US(6),UGAB=B A 逆反律(AB)(BC)=A C 假言三段论A(y)=xA(x)全称推广规则得证第41页/共171页2023/3/2442一阶谓词逻辑的特点优点（1）自然性 谓词逻辑是一种接近于自然语言的形式语言，用它表示的知识比较容易理解；（2）精确性 谓词逻辑是二值逻辑，其谓词公式的真值只有“真”与“假”两个，因此可以用它表示精确的知识。（3）容易实现 用谓词逻辑表示的知识可以容易地转换为计算机的内部形式，分析过程容易在计算机上实现。缺点（1）效率低 用谓词逻辑表示知识时，把推导与知识的语义分开，使得推理过程变长，推
26、理规则太多，中间结论呈指数增长，实施困难。（2）灵活性差 谓词逻辑表示法只能表示精确的知识，不能表示不精确的知识，而人类的知识中有许多不精确或是模糊的知识，使得表示知识的范围受到了限制。第42页/共171页2023/3/24435.2 5.2 归结演绎推理5.2.1 子句集5.2.2 命题逻辑中的归结原理5.2.3 替换与合一5.2.4 谓词逻辑中的归结原理第43页/共171页2023/3/24445.2.15.2.1子句集(1)(1)定义1：原子谓词公式及其否定称为文字 若干个文字的一个析取式称为一个子句 由r个文字组成的子句叫r-文字子句 1-文字子句叫单元子句 不含任何文字的子句称为空子
27、句，记为或NIL。例如：D(y)I(a)P Q R I(z)R(z)第44页/共171页2023/3/24455.2.15.2.1子句集(2)(2)谓词公式例 xyP(x,y)yQ(x,y)R(x,y)子句集例 P(x,f(x)Q(x,g(x),P(y,f(y)R(y,g(y)谓词公式与子句集有哪些区别？“”作用原子谓词没有量词(、)合取范式元素之间变元不同定义2：对一个谓词公式G，通过以下步骤所得的子句集 S，称为G的子句集（clauses）。集合形式没有蕴含词、等值词第45页/共171页2023/3/24465.2.15.2.1子句集(3)(3)例5.7：x y P(x，y)yQ(x,y)
28、R(x,y)由第一步可得：x y P(x，y)y Q(x,y)R(x,y)1、消蕴含词和等值词理论根据：AB A B A B (A B)(B A)蕴含等价式问题:蕴含式yP(x，y)yQ(x,y)R(x,y)的前件是？1：y P(x，y)2：P(x，y)第46页/共171页2023/3/24475.2.15.2.1子句集(4)(4)“”作用原子谓词没有量词(、)合取范式元素之间变元不同集合形式没有蕴含词、等值词第47页/共171页2023/3/24485.2.15.2.1子句集(5)(5)x y P(x，y)y Q(x,y)R(x,y)2、移动否定词作用范围，使其仅作用于原子公式理论根据：(A
29、)A (A B)A B (A B)A B xP(x)xP(x)xP(x)xP(x)双重否定律摩根定律量词转换定律=x y P(x，y)y Q(x,y)R(x,y)=x y P(x，y)y(Q(x,y)R(x,y)=x y P(x，y)y Q(x,y)R(x,y)第48页/共171页2023/3/24495.2.15.2.1子句集(6)(6)“”作用原子谓词没有量词(、)合取范式元素之间变元不同集合形式没有蕴含词、等值词第49页/共171页2023/3/24505.2.15.2.1子句集(7)(7)=x y P(x，y)zQ(x,z)R(x,z)3、适当改名，使变量标准化即：对于不同的约束，对应
30、于不同的变量x y P(x，y)y Q(x,y)R(x,y)问题:不同辖域的相同变元对应的约束相同吗?第50页/共171页2023/3/24515.2.15.2.1子句集(8)(8)4、消去存在量词(Skolem化）,同时进行变元替换 原则：若该存在量词不在任何全称量词的辖域内，则用一 个常量符号代替该存在量词辖域内的相应约束变元，这个常量叫Skolem常量；若该存在量词在全称量词的辖域内，则用这些全 称量词指导变元的一个函数代替该存在量词辖域 内的相应约束变元，这样的函数称为Skolem函数。理论依据：xA（x）=A（y）y是个体域中某一确定的元素。存在指定规则第51页/共171页2023/
31、3/24525.2.15.2.1子句集(9)(9)问题:为什么受全称量词约束的要用Skolem函数替换?而不能用常量替换？x yM（y，x）：对任意一个人x，都存在一个y，y是x的妈妈。若去掉存在量词用常量a代替y，则变为：x M（a，x）：a是所有人的妈妈。实际上，引入Skolem函数，是由于存在量词在全称量词的辖域之内，其约束变元的取值完全依赖于全称变量的取值。而Skolem函数反映了这种依赖关系。第52页/共171页2023/3/24535.2.15.2.1子句集(10)(10)x y P(x，y)zQ(x,z)R(x,z)=xP(x，f(x)Q(x，g(x)R(x，g(x)=P(x，f
32、(x)Q(x,g(x)R(x,g(x)5、消去所有全称量词。理论依据：xA（x）=A（y）y是个体域中任一确定的元素。全称指定规则第53页/共171页2023/3/24545.2.15.2.1子句集(11)(11)子句集的特征“”作用原子谓词没有量词(、)合取范式元素之间变元不同集合形式没有蕴含词、等值词第54页/共171页2023/3/24555.2.15.2.1子句集(12)(12)=P(x，f(x)Q(x,g(x)P(x，f(x)R(x,g(x)6、化公式为合取范式 理论依据：A（B C）（A B）（A C）（A B）C （A C）（B C）P(x，f(x)Q(x,g(x)R(x,g(x
33、)分配律第55页/共171页2023/3/24565.2.15.2.1子句集(13)(13)子句集的特征“”作用原子谓词没有量词(、)合取范式元素之间变元不同集合形式没有蕴含词、等值词第56页/共171页2023/3/24575.2.15.2.1子句集(14)(14)=P(x，f(x)Q(x,g(x)P(y，f(y)R(y,g(y)7、适当改名，使子句间无同名变元=P(x，f(x)Q(x,g(x),P(y，f(y)R(y,g(y)8、消去合取词，以子句为元素组成一个集合S=P(x，f(x)Q(x,g(x)R(x,g(x)第57页/共171页2023/3/24585.2.1 5.2.1 子句集-
34、小结消去蕴含词和等值词使否定词仅作用于原子公式使量词间不含同名指导变元消去存在量词消去全称量词化公式为合取范式子句间无同名变元组成一个集合“”作用原子谓词没有量词(、)合取范式元素之间变元不同集合形式没有蕴含词、等值词蕴含等价式双重否定律、摩根定律、量词转换律存在指定、依赖关系全称指定分配律第58页/共171页2023/3/24595.2.1 5.2.1 子句集-练习（1 1）练习：用谓词公式表示下述命题。已知前提：（1）自然数都是大于零的整数。（2）所有整数不是偶数就是奇数。（3）偶数除以2是整数。结论：所有自然数不是奇数就是除以2为整数的数。化F1 F2 F3 G的子句集。F1:x(N(x
35、)GZ(x)I(x)F2:x(I(x)(E(x)O(x)F3:x(E(x)I(s(x)G:x(N(x)(I(s(x)O(x)第59页/共171页2023/3/24605.2.1 5.2.1 子句集-练习（2 2）F1:x(N(x)GZ(x)I(x)由(1)得x(N(x)(GZ(x)I(x)x(N(x)I(x)(N(x)GZ(x)由(5)得(N(x)I(x)(N(x)GZ(x)由(7)得(N(x)I(x)(N(y)GZ(y)由(8)得N(x)I(x),N(y)GZ(y)F2:x(I(x)(E(x)O(x)由(1)得x(I(x)(E(x)O(x)由(5)得I(z)E(z)O(z)由(8)得I(z)
36、E(z)O(z)第60页/共171页2023/3/24615.2.1 5.2.1 子句集-练习（3 3）F3:x(E(x)I(s(x)由(1)得x(E(x)I(s(x)由(5)得E(x)I(s(x)由(8)得E(u)I(s(u)G:x(N(x)(I(s(x)O(x)由(1)得x(N(x)(I(s(x)O(x)由(2)得x(N(x)(I(s(x)O(x)x(N(x)I(s(x)O(x)由(4)得N(a)I(s(a)O(a)由(8)得N(a),I(s(a),O(a)第61页/共171页2023/3/24625.2.1 5.2.1 子句集-练习（4 4）解：F1F2F3G的子句集为（1）N(x)GZ
37、(x)（2）N(y)I(y)（3）I(z)E(z)O(z)（4）E(u)I(s(u)（5）N(a)（6）O(a)（7）I(s(a)第62页/共171页2023/3/24635.2.1 5.2.1 子句集-练习应用归结原理证明定理（1）N(x)GZ(x)（2）N(y)I(y)（3）I(z)E(z)O(z)（4）E(u)I(s(u)（5）N(a)（6）I(s(a)（7）O(a)（8）E(a)4,6,a/u（9）I(a)E(a)3,7,a/z（10）I(a)8,9（11）N(a)2,10（12）5,11第63页/共171页2023/3/24645.2.1 5.2.1 子句集(18)(18)Skole
38、m标准型 在求子句集的过程中，消去存在量词之后，把所有全称量词都依次移到式子的最左边（或者把所有的量词都依次移到式子最左边，再消去存在量词），再将右部的式子化为合取范式，这样得到的式子就是原公式的Skolem标准型。x y P(x,y)zQ(x,z)R(x,z)=x P(x,f(x)Q(x,g(x)R(x,g(x)=x 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(y，f(y)R(y,g(y)消去合取词和全称量词，就得到了原公式的子句集第64页/共171页2023/3/24655.2.1 5.2.1 子句集(19)(19)例5.8设消去存
39、在量词 用 a 代替x 用 f(y,z)代替u 用g(y,z,v)代替w得到G的Skolem标准型进而得G的子句集为：一个谓词公式的子句集也可以通过求前束范式（如果谓词公式中一切量词都位于该公式最左边，不含否定词，且量词的辖域都延伸到公式末端），再求Skolem标准型而得到。第65页/共171页2023/3/24665.2.1 5.2.1 子句集(20)(20)引入Skolem函数，是由于存在量词在全称量词的辖域内，其约束变元的取值完全依赖于全称量词的取值。Skolem函数反映了这种依赖关系。但Skolem标准型与原公式一般并不等价。有公式：G xP(x)它的Skolem标准型是 G P(a)
40、我们给出如下的解释I：D0,1,a/0,P(0)/F,P(1)/T 在此解释下，GT,G F第66页/共171页2023/3/24675.2.1 5.2.1 子句集(21)(21)定理1：谓词公式G不可满足当且仅当其子句集S不可满足定义3：子句集S是不可满足的，当且仅当其全部子句的 合取式是不可满足的。谓词公式正确性证明谓词公式否定式不可满足性证明谓词公式对应子句集的不可满足性证明第67页/共171页2023/3/24685.2.2 5.2.2 命题逻辑中的归结原理(1)(1)归结原理的提出 归结原理(principle of resolution)又称消解原理,1965年鲁滨逊（J.A.Ro
41、binson）提出，从理论上解决了定理证明问题。归结原理提出的是一种证明子句集不可满足性，从而实现定理证明的一种理论及方法。归结原理的基本原理是采用反证法（反演推理方法）归结算法是一节谓词逻辑中的半可判定算法，对一阶逻辑中任意恒真公式使用归结原理，总可以在有限步内给以判定（证明其为永真）对不知该公式是否为恒真时，使用归结原理得不到任何结论第68页/共171页2023/3/24695.2.2 5.2.2 命题逻辑中的归结原理(2)(2)定义4 设L为一个文字，则L与L为互补文字。定义5 设C1、C2是命题逻辑中的两个子句，C1中有文字L1、C2中有文字L2、且L1与L2互补，从C1、C2中分别删
42、除L1、L2，再将剩余部分析 取起来，构成的新子句为C12，则C12为C1、C2的 归结式，C1、C2称为其归结式的亲本子句，称 L1、L2 为消解基。例5.9设，则C1、C2的归结式为：第69页/共171页2023/3/24705.2.2 5.2.2 命题逻辑中的归结原理(3)(3)定理2 归结式是其亲本子句的逻辑结果。证明：设C1=LC1，C2=L C2 其中C1、C2都是文字的析取式。C1、C2的归结式为C1 C2 C1、C2的逻辑结果为：C1=C1L=C1 L C2=L C2=LC2 由假言三段论可得：C1 C2=（C1L）（LC2）=C1 C2=C1 C2命题逻辑中的归结原理：第70
43、页/共171页2023/3/24715.2.2 5.2.2 命题逻辑中的归结原理(4)(4)例5.10 用归结原理验证分离规则和拒取式 A(AB)B (AB)B A 解 A(AB)A(AB)B (AB)B (AB)(B)A 第71页/共171页2023/3/24725.2.2 5.2.2 命题逻辑中的归结原理(5)(5)类似的可以验证其他推理规则。这说明，归结原理可以代替其他所有的推理规则，而且推理步骤比较机械，为机器推理提供了方便。由归结原理可知：L L NIL 另外我们知道：L L F（假），也就是 NIL F 空子句就是恒假子句第72页/共171页2023/3/2473补充：定理1 G为
44、F1,F2,，Fn的逻辑结论，当且仅当 （F1 F2 Fn）=G定理2 G为F1,F2,，Fn的逻辑结论，当且仅当 (F1 F2 Fn)G是不可满足的。第73页/共171页2023/3/24745.2.2 5.2.2 命题逻辑中的归结原理(6)(6)利用归结原理证明命题公式的思路先求出要证明的命题公式的否定式的子句集S；然后对子句集S（一次或者多次）使用归结原理；若在某一步推出了空子句，即推出了矛盾，则说明子句集S是不可满足的，从而原否定式也是不可满足的，进而说明原公式是永真的。第74页/共171页2023/3/24755.2.25.2.2命题逻辑中的归结原理(7)(7)推出空子句就说明子句集
45、不可满足，原因是：空子句就是F，推出空子句就是推出了F。归结原理是正确的推理形式，由正确的推理形式推出了F，则说明前提不真，即归结出空子句的两个亲本子句至少有一个为假。如果这两个亲本子句都是原子句集S中的子句，即说明原子句集S不可满足。（因子句间为合取关系）如果这两个亲本子句不是或不全是S中的子句，那么它们必定是某次归结的结果。同样的道理向上回溯，一定会推出原子句集中至少有一个子句为假，从而说明S不可满足。第75页/共171页2023/3/24765.2.2 5.2.2 命题逻辑中的归结原理(8)(8)推论 设C1、C2是子句集S的两个子句，C12是它们的归结式，则（1）若用C12来代替C1、
46、C2，得到新的子句集S1，则由S1不可满足性可以推出原子句集S的不可满足性。即 （2）若用C12加入到S中，得到新的子句集S2，则S2与原S的同不可满足。即S1的不可满足性=S不可满足S2的不可满足性S不可满足第76页/共171页2023/3/24775.2.2 5.2.2 命题逻辑中的归结原理(9)(9)例5.12设公理集：P,(PQ)R,(SU)Q,U求证：R化子句集：(PQ)R=(PQ)R=PQR(SU)Q=(SU)Q=(SU)Q=(SQ)(UQ)=SQ,UQ子句集：(1)P(2)PQR(3)SQ(4)UQ(5)U(6)R（目标求反）第77页/共171页2023/3/24785.2.2
47、5.2.2 命题逻辑中的归结原理(10)(10)子句集：(1)P(2)PQR(3)SQ(4)TQ(5)T(6)R（目标求反）归结：(7)PQ (2,6)(8)Q (1,7)(9)T (4,8)(10)NIL (5,9)PQRRPQPQTQTTNIL第78页/共171页2023/3/24795.2.2 5.2.2 命题逻辑中的归结原理(11)(11)例5.11 证明子句集P Q,P,Q是不可满足。证明：子句集：(1)P Q(2)P(3)Q归结：(4)Q 由（1）和（2）(5)NIL由（4）和（5）得证第79页/共171页2023/3/24805.2.3 5.2.3 替换与合一(1)(1)问题 在
48、一阶谓词中应用消解原理，因为谓词逻辑中的子句含有个体变元，所以可能无法直接找到互否文字的子句对 例如：P(x)Q(z),P(f(y)R(y)P(x)Q(y),P(a)R(z)解决方法 对个体变元做适当替换 例如：P(f(y)Q(z),P(f(y)R(y)P(a)Q(y),P(a)R(z)第80页/共171页2023/3/24815.2.3 5.2.3 替换与合一(2)(2)定义6 一个替换（Substitution）是形如t1/x1,t2/x2,tn/xn的有限集合，其中 t1,t2,tn是项，称为替换的分子；x1,x2,xn是互不相同的个体变元，称为替换的分母；ti,xi不同，xi不循环出现
49、在tj中；(i,j=1,2,n)ti/xi 表示用ti替换xi。若其中t1,t2,tn是不含变元的项（称为基项）时，该替换为 基替换；没有元素的替换称为空替换，记作，表示不作任何替换。例：a/x,g(a)/y,f(g(b)/z g(y)/x,f(x)/y是一个替换不是一个替换，x与y出现了循环替换第81页/共171页2023/3/2482回顾定义项（1）个体常元和变元都是项。（2）f是n元函数符号，若t1,t2,tn是项，则f(t1,t2,tn)是项。（3）只有有限次使用(1),(2)得到的符号串才是项原子公式：设P是n元谓词符号，t1,t2,.,tn是项,则P(t1,t2,.,tn)是原子谓
50、词公式文字：原子谓词公式及其否定式子句：若干文字的析取称为一个子句第82页/共171页2023/3/24835.2.3 5.2.3 替换与合一(3)(3)表达式：项、原子公式、文字、子句的统称。基表达式：没有变元的表达式。子表达式：出现在表达式E中的表达式称为E的子表达式。定义7 设=t1/x1,t2/x2,tn/xn是一个替换，E是一个表达式，对E实施替换，即把E中出现的个体变元xj都用tj替换，记为E,所得的结果称为E在下的例（instance）。例如：若=a/x,f(b)/y,c/z,G=P(x,y,z)G=P(a,f(b),c)第83页/共171页2023/3/24845.2.3 5.