第5章 基于谓词逻辑的机器推理 2019/2/19

目录 5.0 机器推理概述 5.1 一阶谓词逻辑 5.2 归结演绎推理 5.3 应用归结原理求取问题答案 5.4 归结策略 5.5 归结反演程序举例* 5.6 Horn子句归结与逻辑程序 5.7 非归结演绎推理 2019/2/19

5.0 机器推理概述（1） 机器推理： 就是计算机推理，也称自动推理。它是人工智能的核心课题之一。推理是人脑的一个基本功能和重要功能。几乎所有的人工智能领域都与推理有关。因此，要实现人工智能，就必须将推理的功能赋予机器，实现机器推理。 自动定理证明： 是机器推理的一种重要应用，它是利用计算机证明非数值性的结果，很多非数值领域的任务如医疗诊断、信息检索、规划制定和难题求解等方法都可以转化一个定理证明问题。 2019/2/19

5.0 机器推理概述（2） 自动定理证明的基本方法： 自然演绎法：该方法依据推理规则从前提和公理中可以推出许多定理，如果待证明的定理在其中则定理得证。LT程序、证明平面几何的程序。 判定法：该方法是对一类问题找出统一的计算机上可实现的算法。数学家吴文俊教授——吴氏方法。 人机交互进行定理证明：计算机作为数学家的辅助工具，用计算机帮助人完成手工证明中的难以完成的烦杂的大量计算推理和穷举。四色定理。 定理证明器：它是研究一切可判定问题的证明方法。鲁滨逊的归结原理。 2019/2/19

5.0 机器推理概述（3） 基于归结原理的自动定理证明过程： 定理的自然语言描述 已知前提：（1）自然数都是大于零的整数。 （2）所有整数不是偶数就是奇数。 （3）偶数除以2是整数。 结论：所有自然数不是奇数就是一半为整数的数。 自然语言处理生成谓词公式 定理的谓词公式描述 生成子句集 子句集 应用归结规则＋归结策略 定理得证 2019/2/19

5.0 机器推理概述（4） 本章主要解决以下几个问题： 1、一阶谓词逻辑及基于一阶谓词逻辑的知识表示 2、谓词公式到子句集的转换 3、命题逻辑和谓词逻辑中的归结原理 4、归结策略 2019/2/19

5.1一阶谓词逻辑 5.1.1 谓词、函数、量词 5.1.2 谓词公式 5.1.3 谓词逻辑中的形式演绎推理 2019/2/19

5.1.1谓词、函数、量词（1） 命题（proposition）：是具有真假意义的语句。命题代表人 们进行思维时的一种判断，或者是否定，或者是肯定。 命题可以用命题符号表示。 用命题符号可以表示简单的逻辑关系和推理。 P:今天天气好 Q:去旅游 S1：我有名字 S2：你有名字 PQ表示：如果今天天气好，就去旅游。 此时，如果P（今天天气好）成立，则可以得到结论Q（去旅游） 2019/2/19

5.1.1谓词、函数、量词（2） 对于复杂的知识，命题符号能力不够。 无法把所描述的客观事物的结构及逻辑特征反映出来。 无法把不同事物间的共同特征表达出来。 F：老李是小李的父亲。 S1：我有名字 S2：你有名字 所有的人都有名字： SIS2 S3 … 2019/2/19

5.1.1谓词、函数、量词（3） 谓词(predicate)：一般形式为P（x1, x2 ,…, xn ） 或个体间的关系。 x1， x2 ，…， xn是个体，表示某个独立存 在的事物或者某个抽象的概念。 S(x): x是学生； P(x,y): x是y的双亲。 个体变元的变化范围称为个体域。 包揽一切事物的集合称为全总个体域。 2019/2/19

5.1.1谓词、函数、量词（4） 函数：为了表达个体之间的对应关系，引入数学中函数概念和记法。用形如f(x1，x2，…，xn)来表示个体变元对应的个体y，并称之为n元个体函数，简称函数。 函数 father(x): 值为x的父亲。 谓词D(father(x) ): 表示x的父亲是医生，值为真或假。 符号约定：谓词－大写字母； P(x,y) 函数－小写字母；f(x) 变量－ x、y、z、u、v……； 常量－a、b、c…….。 P(a,Y) 2019/2/19

5.1.1谓词、函数、量词（5） 如：“凡是人都有名字” 用M（x）表示“x是人”，N（x）表示“x有名字” x（M（x）  N（x）） 全称量词 表示“对个体域中所有的（或任一个）个体” 。 记为x 如：“凡是人都有名字” 用M（x）表示“x是人”，N（x）表示“x有名字” x（M（x）  N（x）） 存在量词 表示“在个体域中存在个体”。 记为x 如：“存在不是偶数的整数” 用G（x）表示“x是整数”，E（x）表示“x是偶数”  x（G（x）  ¬ E（x）） 2019/2/19

5.1.1谓词、函数、量词（6） 用谓词表示命题时，一般取全总个体域，再采用使用 限定谓词的方法来指出每个个体变元的个体域。 (1)对全称量词，把限定词作为蕴含式之前件加入。 即 x （P（x）  … ） 例：对于所有的自然数，均有x+y>x x y（ N （x）  N（y）  S(x,y,x)） 例5.2：对于所有的自然数，均有x+y>x 也可以用函数h（x，y）来表示x与y的和 x y（ N （x）  N（y）  G(h(x,y),x)） (2)对存在量词，把限定词作为一个合取项加入。即 x(P(x) …) 例5.3：某些人对某些食物过敏  x  y(M(x)  N(y) G（x，y）） 2019/2/19

5.1.1谓词、函数、量词（7） 用谓词表示命题时，形式并不是固定的。 例5.1：不存在最大的整数，我们可以把它表示为： ¬  x(G(x)   y（G（y）  D（x，y））  x(G(x)   y（G（y）  D（y，x）） 2019/2/19

5.1.1谓词、函数、量词（8） 练习：用谓词公式表示下述命题。 已知前提： （1）自然数都是大于零的整数。 （2）所有整数不是偶数就是奇数。 （3）偶数除以2是整数。 结论：所有自然数不是奇数就是一半为整数的数。 首先定义如下谓词： N(x):x是自然数。 I(x):x是整数。 E(x):x是偶数。 O(x):x是奇数。 GZ(x):x大于零。 s(x):x除以2。 2019/2/19

5.1.1谓词、函数、量词（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))) 所有自然数不是奇数就是一半为整数的数。 G: x (N(x)(I(s(x)) O(x))) 2019/2/19

5.1.2谓词公式（1） 用谓词、量词及真值连结词可以表达相当复杂的命题， 我们把命题的这种符号表达式称为谓词公式。 定义1：项 （1）个体常元和变元都是项。 （2）f是n元函数符号，若t1，t2，…，tn是项，则 f（ t1，t2，…， tn ）是项。 （3）只有有限次使用（1），（2）得到的符号串才是项。 2019/2/19

5.1.2谓词公式（2） 定义2：原子公式 设P为n元谓词符号， t1，t2，…，tn为项， P （ t1 ，t2，…，tn ）称为原子谓词公式，简称原子或原 子公式。 2019/2/19

5.1.2谓词公式（3） 定义3：谓词公式 （1）原子公式是谓词公式。 （2）若A、B是谓词公式，则A，A  B，A  B，A  B， A←→B， xA， xA也是谓词公式。 （3）只有有限步应用（1）（2）生成的公式才是谓词公式。 由项的定义，当t1，t2，…，tn全为个体常元时，所得的原子谓词公式就是原子命题公式（命题符号）。所以全体命题公式也是谓词公式。 谓词公式亦称为谓词逻辑中的合适（式）公式，记为Wff。 2019/2/19

5.1.2谓词公式（4） 辖域：紧接于量词之后被量词作用（即说明）的谓词公式称为该量词的辖域。 指导变元：量词后的变元为指导变元。 约束变元：在一个量词辖域中与该量词的指导变元相同的变元称为约束变元。 自由变元：在一个量词辖域中与该量词的指导变元不同的变元称为自由变元。 （1）  x P（x） （2） y（G（y）  D（x，y）） （3）  x G(x)  P（x） 约束 变元 约束 变元 自由 变元 指导 变元 约束 变元 自由 变元 2019/2/19

5.1.2谓词公式（5） 一个变元在一个公式中既可以约束出现，也可以自由出现，为了避免混淆，通过改名规则改名： 对需要改名的变元，应同时更改该变元在量词及其辖域中的所有出现。 新变元符号必须是量词辖域内原先没有的，最好是公式中也未出现过的。  x G(x)  P（x）  x G(x)  P（y） 2019/2/19

5.1.2谓词公式（6） 谓词公式与命题的区别与联系 谓词公式是命题函数。 一个谓词公式中所有个体变元被量化，谓词公式就变成了一个命题。 从谓词公式得到命题的两种方法：给谓词中的个体变元代入个体常元；把谓词中的个体变元全部量化。 例：P（x）表示“x是素数” x P（x），  x P（x）， P（a）都是命题 2019/2/19

5.1.2谓词公式（7） 一阶谓词：仅个体变元被量化的谓词。 二阶谓词：个体变元被量化，函数符号和谓词符号也被量化。 P  x P（x） 全称命题：  x P(x)等价于P (a1)P(a2) … P(an) 特称命题  x G(x)等价于P (a1)P(a2) …  P (an) 2019/2/19

5.1.2谓词公式（8） 定义4：合取范式（Conjunctive Normal Form） B1  B2  …  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) ) 就是一个合取范式 2019/2/19

5.1.2谓词公式（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) ) 就是一个析取范式 2019/2/19

5.1.2谓词公式（10） 谓词公式的解释 （1）为每个个体常量指派D中的一个元素； （2）为每个n元函数指派一个从Dn到D的映射，其中 设D为谓词公式P的个体域，若对P中的个体常量、函数和谓词按如下规定赋值： （1）为每个个体常量指派D中的一个元素； （2）为每个n元函数指派一个从Dn到D的映射，其中 Dn＝{(x1,x2,…,xn)/x1,x2,…,xn ∈ D} （3）为每个n元谓词指派一个从Dn到{F,T}的映射。 则称这些指派为公式P在D上的一个解释。 2019/2/19

5.1.2谓词公式（11） 例：设个体域D＝{1,2},求公式A＝  x  yP（x，y）在D上的解释，并指出在每一种解释下公式A的真值。 解：公式里没有个体常量和函数，所以直接为谓词指派真值，设为 P（1，1）＝T P（1，2）＝F P（2，1）＝T P（2，2）＝F 这就是A在D上的一个解释。 在此解释下： 当x＝1时有y＝1使P（x，y）的真值为T； 当x＝2时有y＝1使P（x，y）的真值为T； 即对于D中的所有X都有y＝1使P（x，y）的真值为T， 所以在此解释下公式A的真值为T。 2019/2/19

5.1.2谓词公式（12） 例：设个体域D＝{1,2}, 求公式A＝  x P（x） Q（f(x),b）在D上的解释，并指出在每一种解释下公式A的真值。 解：为个体常量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 2019/2/19

5.1.2谓词公式（13） 在此解释下， 当x＝1时有： P(1)=F, Q(f(1),1)=Q(2,1)=F 所以P（x） Q（f(x),b）为T。 当x＝2时有 P(2)=T, Q(f(2),1)=Q(1,1)=T 即对个体域D中的所有x均有P（x） Q（f(x),b），所以公式B在此解释下的真值为T。 2019/2/19

5.1.2谓词公式（14） 定义6：谓词公式在个体域上的永真、永假、可满足 设P为谓词公式，D为其个体域，对于D中的任一解释I： （1）若P恒为真，则称P在D上永真或是D上的永真式。 （2）若P恒为假，则称P在D上永假或是D上的永假式。 （3）若至少有一个解释，可是P为真，则称P在D上是 可满足式。 2019/2/19

5.1.2谓词公式（15） 定义7：谓词公式全个体域上的永真、永假、可满足 设P为谓词公式，对于任何个体域： （1）若P都永真，则称P为永真式。 （2）若P都永假，则称P为永假式。 （3）若P都可满足，则称P为可满足式。 谓词公式的真值与个体域及真值有关，考虑到个体域的 数目和个体域中元素数目无限的情形，所以要通过算法 判断一个谓词公式永真是不可能的，所以称一阶谓词逻 辑是不可判定的。 2019/2/19

5.1.3谓词逻辑中的形式演绎推理（1） 自然演绎推理 常用逻辑等价式 常用逻辑蕴含式 利用一阶谓词推理规则的符号表示形式，可以把关于自然语言的逻辑推理问题，转化为符号表达式的推演变换。这种推理十分类似于人们用自然语言推理的思维过程，因而称为自然演绎推理。 常用逻辑等价式 常用逻辑蕴含式 2019/2/19

常用逻辑等价式（1） 2019/2/19

常用逻辑等价式（2） 2019/2/19

常用逻辑等价式（3） 2019/2/19

常用逻辑等价式（4） 2019/2/19

常用逻辑蕴含式（1) 2019/2/19

常用逻辑蕴含式(2) 2019/2/19

5.1.3谓词逻辑中的形式演绎推理（2） 例5.4 设有前提： （1）凡是大学生都学过计算机； （2）小王是大学生。 例5.4 设有前提： （1）凡是大学生都学过计算机； （2）小王是大学生。 试问：小王学过计算机吗？ 解：令S（x）：x是大学生 M（x）：x学过计算机； a：小王 上面命题用谓词公式表示为： 我们进行形式推理： [前提] [(1),US] xA(x)=>A(y) y是个体域中任一确定元素 [前提] [(2),(3),I3] M(a)，即小王学过计算机。 (A  B)  A => B 2019/2/19

5.1.3谓词逻辑中的形式演绎推理（3） 例5.5 证明 是 和 逻辑 结果。 证： [前提] [(1),US] [(2),US] [前提] 例5.5 证明 是 和 逻辑 结果。 证： [前提] [(1),US] [(2),US] [前提] [(3),(4),I4] (A  B)  ¬ B => ¬ A 拒取式 2019/2/19

(AB)  (BC) => A  B 假言三段论 5.1.3谓词逻辑中的形式演绎推理（4） 例5.6 证明 证： [前提] [(1),US] [(2),E24] AB => ¬B  ¬ A 逆反律 [前提] [(4),US] [(3),(5),I6] (AB)  (BC) => A  B 假言三段论 [(1),UG] A(y) => xA(x) 全称推广规则 2019/2/19

5.2归结演绎推理 5.2.1 子句集 5.2.2 命题逻辑中的归结原理 5.2.3 替换与合一 5.2.4 谓词逻辑中的归结原理 2019/2/19

5.2.1子句集(1) 定义1：原子谓词公式及其否定称为文字 若干个文字的一个析取式称为一个子句 由r个文字组成的子句叫r-文字子句 1-文字子句叫单元子句 不含任何文字的子句称为空子句，记为 或NIL。 例如： ¬D(y) I(a) P Q ¬R ¬I(z)R(z) 2019/2/19

5.2.1子句集(2) 定义2：对一个谓词公式G，通过以下步骤所得的子句集 S，称为G的子句集（clauses）。 例5.7：x { y P(x，y)  ¬ y[Q(x,y) R(x,y)]} 1、消蕴含词和等值词 理论根据：AB ¬A B A B (¬A B) ( ¬B A) 蕴含表达式 由第一步可得： x {¬  y P(x，y)  ¬y[¬ Q(x,y) R(x,y)]} 2019/2/19

5.2.1子句集(3) 理论根据： ¬ (¬A) A ¬(A B) ¬A ¬B ¬(A B) ¬A ¬B 2、移动否定词作用范围，使其仅作用于原子公式 理论根据： ¬ (¬A) A ¬(A B) ¬A ¬B ¬(A B) ¬A ¬B ¬xP(x) x¬P(x) ¬xP(x) x¬P (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)]} 3、适当改名，使变量标准化 即：对于不同的约束，对应于不同的变量 x { y ¬ P(x，y)   z[Q(x,z)  ¬ R(x,z)]} 2019/2/19

¬ P(x，f(x))  [Q(x,g(x))  ¬ R(x,g(x))] 5.2.1子句集(4) 4、 消去存在量词 (Skolem化）,同时进行变元替换 原则：对于一个受存在量词约束的变量，如果它 不受全称量词约束，则该变量用一个常量代替（这 个常量叫Skolem常量），如果它受全称量词约束， 则该变量用一个全称量词指导变元的函数代替（这 个函数叫Skolem函数） 。 x { y ¬ P(x，y)   z[Q(x，z)  ¬ R(x，z)]} => x {¬ P(x，f(x))  [Q(x，g(x))  ¬ R(x，g(x))]} 5、消去所有全称量词。 ¬ P(x，f(x))  [Q(x,g(x))  ¬ R(x,g(x))] 2019/2/19

5.2.1子句集(5) 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))] [¬ P(x，f(x))  Q(x,g(x))]  [¬ P(x，f(x))  ¬ R(x,g(x))] 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)) , ¬ P(y，f(y))  ¬ R(y,g(y))} 2019/2/19

5.2.1子句集(6) 元素只是文字的析取；（1） 否定符只作用于单个文字；（2） 元素间默认为合取。（6，7，8） 化子句集的步骤： 1、消去蕴含词和等值词。 2、使否定词仅作用于原子公式。 3、适当改名使量词间不含同名指导变元。 4、消去存在量词。 5、消去全称量词。 6、化公式为合取范式。 7、适当改名，使子句间无同名变元。 8、消去合取词，以子句为元素组成一个集合S。 子句集：无量词约束；（3，4，5） 元素只是文字的析取；（1） 否定符只作用于单个文字；（2） 元素间默认为合取。（6，7，8） 2019/2/19

5.2.1子句集(7) F1: x (N(x)GZ(x)  I(x)) 练习：用谓词公式表示下述命题。 已知前提： （1）自然数都是大于零的整数。 （2）所有整数不是偶数就是奇数。 （3）偶数除以2是整数。 结论：所有自然数不是奇数就是一半为整数的数。 化F1  F2  F3  ¬G的子句集。 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))) 2019/2/19

5.2.1子句集(8) 解：F1  F2  F3  ¬G的子句集为 （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） ¬O(a) （7） ¬I(s(a)) 2019/2/19

5.2.1子句集(9) Skolem标准型 在求子句集的过程中，消去存在量词 之后，把所有全称量词都依次移到式子的最左边（或者 把所有的量词都依次移到式子最右边，再消去存在量 词），再将右部的式子化为合取范式，这样得到的式 子就是Skolem标准型。 x { y ¬ P(x，y)   z[Q(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))} 2019/2/19

5.2.1子句集(10) 例5.8设 消去存在量词 用a代替x 用f（y，z）代替u 用g（y，z，v）代替w 得到G的Skolem标准型 2019/2/19

5.2.1子句集(11) 域内，其约束变元的取值完全依赖于全称量词的取值。 Skolem反映了这种依赖关系。 有公式： G ＝ xP(x) 它的Skolem标准型是 G’ ＝ P(a) 我们给出如下的解释I： D＝{0,1}, a/0, P(0)/F, P(1)/T 在此解释下，G＝T,G’ ＝ F 2019/2/19

5.2.1子句集(12) 定理1：谓词公式G不可满足当且仅当其子句集S不可满 足。 定义3：子句集S是不可满足的，当且仅当其全部子句的 合取式是不可满足的。 2019/2/19

5.2.2命题逻辑中的归结原理(1) 归结原理的提出 归结原理(principle of resolution)又称消解原理,1965年鲁滨逊（J.A.Robinson）提出，从理论上解决了定理证明问题。归结原理提出的是一种证明子句集不可满足性，从而实现定理证明的一种理论及方法。 2019/2/19

5.2.2命题逻辑中的归结原理(2) 定义4 设L为一个文字，则L与¬L为互补文字。 定义5 设C1， C2是命题逻辑中的两个子句， C1中有文字L1 ，C2中有文字L2 ，且L1与L2互补， 从C1 、 C2中分别删除L1 、L2 ， 再将剩余部分析取起来， 记构成的新子句为C1 2，则C1 2为C1 、 C2的归结式， C1 、 C2称为其归结式的亲本子句， 称L1 、L2 为消解基。 例5.9 设 ，则C1 、 C2的归结式为： 2019/2/19

5.2.2命题逻辑中的归结原理(3) 定理2 归结式是其亲本子句的逻辑结果。 证明：设C1=LC1’ ， C2 = ¬ L  C2’ 定理2 归结式是其亲本子句的逻辑结果。 证明：设C1=LC1’ ， C2 = ¬ L  C2’ 其中C1’ 、 C2’ 都是文字的析取式。 则C1 C2的逻辑结果为 C1= C1 ’L= ¬ C1 ’ → L C2= ¬ L  C2’= L → C2’ 由假言三段论得： C1 ∧ C2 = （¬ C1 ’ → L） ∧ （ L → C2’） => ¬ C1 ’ → C2’ = C1 ’  C2’ 则C1 C2的归结式为C1 ’  C2’ 命题逻辑中的归结原理： 2019/2/19

5.2.2命题逻辑中的归结原理(4) 例5.10 用归结原理验证分离规则和拒取式 A∧(A→B) ＝＞ B (A→B)∧﹁ B ＝＞﹁ A 例5.10 用归结原理验证分离规则和拒取式 A∧(A→B) ＝＞ B (A→B)∧﹁ B ＝＞﹁ A 解 A∧(A→B) ＝ A∧(﹁ A∨B) ＝＞ B (A→B)∧﹁ B ＝ (﹁ A∨B)∧(﹁ B) ＝＞ ﹁ A 2019/2/19

5.2.2命题逻辑中的归结原理(5) 类似的可以验证其他推理规则。这说明，归结原理可以代替其他所有的推理规则，而且推理步骤比较机械，为机器推理提供了方便。 由归结原理可知 ：L ∧ ¬ L ＝NIL 另外我们知道：L ∧ ¬ L ＝F（假），也就是 NIL F 2019/2/19

5.2.2命题逻辑中的归结原理(6) 利用归结原理证明命题公式的思路 先求出要证明的命题公式的否定式的子句集S； 2019/2/19

5.2.2命题逻辑中的归结原理(7) 推出空子句就说明子句集不可满足，原因是： 空子句就是F，推出空子句就是推出了F。 而这两个亲本子句如果都是原子句集S中不可满足。 如果这两个亲本子句不是或不全是S中的子句，那么它们必定是某次归结的结果。 同样的道理向上回溯，一定会推出原子句集中至少有一个子句为假，从而说明S不可满足。 2019/2/19

S2的不可满足性<=> S不可满足 5.2.2命题逻辑中的归结原理(8) 推论 设C1， C2是子句集S的两个子句，C1 2是 它们的归结式，则 （1）若用C1 2来代替C1， C2 ，得到新的子句集S1 ，则由S1不可满 足性可以推出原子句集S的不可满足性。即 S1的不可满足性=> S不可满足 （2）若用C1 2加入到S中，得到新的子句集S2 ，则S2与原S的同不 可满足。即 S2的不可满足性<=> S不可满足 2019/2/19

5.2.2命题逻辑中的归结原理(9) 例5.12 设公理集：P, (PQ) R, (ST) Q, T 求证：R 化子句集： => (¬SQ) (¬TQ) => {¬SQ, ¬TQ} 子句集： (1) P (2) ¬P¬QR (3) ¬SQ (4) ¬TQ (5) T (6) ¬R（目标求反） 2019/2/19

5.2.2命题逻辑中的归结原理(10) 子句集： (1) P (2) ¬P¬QR (3) ¬SQ (4) ¬TQ (5) T NIL 归结： (7) ¬P¬Q (2, 6) (8) ¬Q (1, 7) (9) ¬T (4, 8) (10)NIL (5, 9) 2019/2/19

5.2.2命题逻辑中的归结原理(11) 练习：证明子句集{P  ¬ Q, ¬ P, Q}是不可满足。 2019/2/19

5.2.3替换与合一(1) 问题 解决方法 对个体变元做适当替换 例如： P(x)Q(z), ¬ P(f(y))R(y) 在一阶谓词中应用消解原理，无法直接找到互否文字的子句对 例如： 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(y) 2019/2/19

5.2.3替换与合一(2) 定义6 一个替换（Substitution）是形如 {t1/x1, t2/x2, …, tn/xn}的有限集合， 其中t1, t2, …, tn是项，称为替换的分子； x1, x2, …, xn是互不相同的个体变元，称为替换的分母； ti, xi不同， xi不循环出现在tj中； ti/xi 表示用ti替换xi 。 若其中t1, t2, …, tn是不含变元的项（称为基项）时， 该替换为基替换； 没有元素的替换称为空替换，记作ε，表示不作任何替换。 {a/x,g(a)/y,f(g(b))/z}就是一个替换 {g(y)/x,f(x)/y}就不是一个替换，x与y出现了循环替换 2019/2/19

5.2.3替换与合一(3) 基表达式：没有变元的表达式。 子表达式：出现在表达式E中的表达式称为E的子表达式。 表达式：项、原子公式、文字、子句的统称。 基表达式：没有变元的表达式。 子表达式：出现在表达式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) 2019/2/19

5.2.3替换与合一(4) 定义8 设θ＝ {t1/x1, t2/x2, …, tn/xn}， λ＝ {u1/y1, u2/y2, …, un/yn}是两个替换，则将 {t1 λ /x1, t2 λ /x2, …, tn λ /xn ，u1/y1, u2/y2, …, un/yn} 中符合下列条件的元素删除 （1） ti λ /xi 当ti λ ＝ xi （2） ui/yi 当yi ∈ {x1,…, xn} 这样得到的集合为 θ 与λ 的复合或乘积，记为θ •λ 。 例：设θ= {f(y)/x,z/y}, λ ={a/x,b/y,y/z} {t1 λ /x1, t2 λ /x2, u1/y1, u2/y2, u3/yn} ={f(b)/x，y/y，a/x，b/y，y/z} 从而 θ •λ ={f(b)/x， y/z} 2019/2/19

5.2.3替换与合一(5) 定义9 设S＝{F1,F2,…,Fn} 是一个原子谓词公式集，若 为S的一个合一，称S为可合一的。 例： {P(x, f(y), B), P(z, f(B), B)} 替换s={A/x, B/y, A/z}是一个合一, 因为： P(x, f(y), B)s= P(A, f(B), B) P(z, f(B), B)s= P(A, f(B), B) 替换s={z/x, B/y}和替换s={x/z, B/y}也都是合一。 一个公式的合一一般不唯一 2019/2/19

5.2.3替换与合一(6) 定义10 设σ是原子公式集S的一个合一，如果对S的任何一个合一 θ都存在一个替换λ，使得 θ ＝ σ •λ 则称σ为S的最一般合一(Most General Unifier),简称MGU。 例： 设S＝{P(u, y, g(y)), P(x, f(u), z)},S有一个最一般合一 σ＝{u/x，f(u)/y，g(f(u))/z} 对S的任一合一，例如： θ＝{a/x，f(a)/y，g(f(a))/z，a/u} 存在一个替换 λ＝{a/u} 使得 θ ＝ σ •λ 一个公式集的MGU也是不唯一的。 2019/2/19

5.2.3替换与合一(7) 定义11 设S是一个非空的具有相同谓词名的原子公式集， 从S中各公式左边的第一项开始，同时向右比较， 直到发现第一个不都相同的项为止，用这些项 的差异部分组成的集合就是S的一个差异集。 例：设S＝{P(x,y,z),P(x,f(a),h(b))} 根据上述差异集定义我们可以看出S有两个差异集： D1＝{y,f(a)} D2＝{z,h(b)} 2019/2/19

5.2.3替换与合一(8) 合一算法（Unification algorithm） Step1：置k＝0，Sk＝S， σk ＝ε； Step2：若Sk只含有一个谓词公式，则算法停止， σk就是最一般 合一； Step3：求Sk的差异集Dk； Step4：若中存在元素xk和tk ，其中xk是变元， tk是项且xk不在tk 中出现，则置Sk ＋1＝Sk{tk/ xk} σk+1= σk {tk/ xk} k＝k+1然后转Step2； Step5：算法停止，S的最一般合一不存在。 2019/2/19

5.2.3替换与合一(9) 例：求公式集S＝{P(a,x,f(g(y))),P(z,h(z,u),f(u))}的最一般合一。 解 k＝0； S0＝S， σ0＝ε，D0＝{a,z} σ1＝ σ0·{a/z}= {a/z} S1= S0·{a/z} = {P(a,x,f(g(y))),P(a,h(a,u),f(u))} k＝1； D1={x, h(a,u)} σ2= σ1·{h(a,u) /x}＝ {a/z,h(a,u) /x} S2= S1·{a/z, h(a,u) /x} = {P(a, h(a,u) ,f(g(y))), P(a,h(a,u),f(u))} k＝2； D2＝{g(y),u} σ3＝ {a/z ,h(a,u) /x ,g(y),u} S3= S2·{g(y),u} = {P(a,h(a,g(y)),f(g(y)))} S3单元素集 ， σ3为MGU。 2019/2/19

5.2.3替换与合一(10) 例5.17 判定S=｛P(x,x),P(y,f(y))｝是否可合一？ 解 k=0: S0=S,σ0=ε, S0不是单元素集，D0=｛x,y｝ σ1=σ0·｛y/x｝=｛y/x｝ S1=S0｛y/x｝=｛P(y,y),P(y,f(y))｝ k=1: S1 不是单元素集，D1=｛y,f(y)｝，由于变元y在项f(y)中出现，所以算法停止，S不存在最一般合一。 2019/2/19

5.2.3替换与合一(11) 定理3 (合一定理) S是非空有限可合一的公式集， 则合一算法总在Step2停止，且最后的σk 一定是S的最一般合一（MGU）。 对任一非空有限可合一的公式集，一定存在最一般合一，而且 用合一算法一定能找到最一般合一。 从合一算法可以看出，一个公式集S的最一般合一可能是不唯一的，因为如果差异集Dk=｛ak,bk｝，且ak和bk都是个体变元，则下面两种选择都是合适的： σk+1=σk·｛bk/ak｝或σk+1=σk·｛ak/bk｝ 2019/2/19

5.2.4谓词逻辑中的归结原理(1) 定义12 C1，C2为无相同变元的子句； L1，L2为其中的两个文字， L1和¬L2有最一般合一σ； （C1 σ －{L1 σ}） ∪ （ C2 σ－ {L2 σ}） 其中C1，C2称作归结式的亲本子句； L1，L2称作消解文字。 例： P(x)Q(y), ¬P(f(z))R(z) => Q(y)R(z) 2019/2/19

5.2.4谓词逻辑中的归结原理(2) 例5.18 设C1=P(x)∨Q(x),C2= ¬ P(a)∨R(y)，求C1,C2的归结式。 解 取L1=P(x),L2=P(a), 则L1与L2的最一般合一σ=｛a/x｝， 于是,(C1σ-｛L1σ｝)∪(C2σ-｛L2σ｝) =(｛P(a),Q(a)｝-｛P(a)｝)∪(｛P(a),R(y)｝-｛P(a)｝) =｛Q(a),R(y)｝ =Q(a)∨R(y) 所以，Q(a)∨R(y)是C1和C2的二元归结式。 2019/2/19

5.2.4谓词逻辑中的归结原理(3) 例5.19 设C1=P(x,y)∨Q(a),C2= ¬ Q(x)∨R(y),求C1,C2的归结式。 解 由于C1,C2中都含有变元x,y，所以需先对其中一个进行改名, 方可归结（归结过程是显然的，故从略）。 还需说明的是，如果在参加归结的子句内部含有可合一的文字， 则在进行归结之前，也应对这些文字进行合一，从而使子句达到 最简。 2019/2/19

5.2.4谓词逻辑中的归结原理(4) 例如，设有两个子句： C1=P(x)∨P(f(a))∨Q(x) C2= ¬ P(y)∨R(b) 可见,在C1 ,C2中有可合一的文字P(x)与P(f(a)) 取替换θ={f(a)/x} 则得 C1θ=P(f(a))∨Q(f(a)) 现在再用C1θ与C2进行归结，从而得到C1与C2的归结式 Q(f(a))∨R(b) 2019/2/19

5.2.4谓词逻辑中的归结原理(5) 定义13 子句C中，两个或两个以上的文字有一个最 一般合一σ，则称C σ为C的因子，若C σ 例5.20： C＝P(x) P(f(y))  ¬Q(x), σ={f((y)/x} C σ ＝ P(f(y))  ¬Q(x)是C的因子。 2019/2/19

5.2.4谓词逻辑中的归结原理(6) 定义14 子句的C1，C2消解式，是下列二元消解式之一: （1） C1和C2的二元消解式； 2019/2/19

5.2.4谓词逻辑中的归结原理(7) 定理4 谓词逻辑中的消解（归结）式是它的亲本子句 的逻辑结果。 谓词逻辑的推理规则： 定理4 谓词逻辑中的消解（归结）式是它的亲本子句 的逻辑结果。 谓词逻辑的推理规则： C1  C2 ＝>（C1 σ －{L1 σ}） ∪ （ C2 σ－ {L2 σ}） 其中C1 ， C2 是两个无相同变元的子句，L1，L2分别是 C1 ，C2中的文字σ为 L1 和L2 的最一般合一。这个规 则称为谓词逻辑中的消解原理（或归结原理）。 2019/2/19

5.2.4谓词逻辑中的归结原理(8) 例5.21求证G是A1和A2的逻辑结果。 A1： (x)(P(x)(Q(x) R(x))) A2 ：(x)(P(x)  S(x)) G：(x)(S(x)R(x)) 证：利用归结反演法，先证明A1  A2 ¬G是不可满足的。 求子句集： (1) ¬P(x) Q(x) (2) ¬P(y) R(y) (3)P(a) (4)S(a) (5) ¬S(z)  ¬ R(z) (¬G) A1 S A2 2019/2/19

5.2.4谓词逻辑中的归结原理(9) 子句集S (1) ¬P(x) Q(x) (2) ¬P(y) R(y) (3)P(a) (4)S(a) (5) ¬S(z)  ¬ R(z) 应用消解原理，得： (6)R(a) [(2),(3), σ1={a/y}] (7) ¬ R(a) [(4),(5), σ2 ={a/z}] (8)Nil [(6),(7)] 所以S是不可满足的，从而G是A1和A2的逻辑结果。 2019/2/19

5.2.4谓词逻辑中的归结原理(10) 例5.22 设已知： （1）能阅读者是识字的； （2）海豚不识字； （3）有些海豚是很聪明的。 试证明：有些聪明者并不能阅读。 证 首先定义如下谓词： R(x):x能阅读。 L(x):x能识字。 I(x):x是聪明的。 D(x):x是海豚。 将上述各语句翻译成谓词公式： (1) (x)(R(x)L(x)) (2) (x)(D(x)¬L(x)) 已知条件 (3) (x) (D(x)  I(x)) (4) (x) (I(x)  ¬ R(x)) 需证结论 2019/2/19

5.2.4谓词逻辑中的归结原理(11) 用归结反演法来证明，求题设与结论否定的子句集，得： (1) ¬ R(x)  L(x) (2) ¬ D(y)  ¬L(y) （改名） (3) D(a) (4) I(a) (5) ¬ I(z)  R(z) ¬ I(z)  R(z) R(a) L(a) ¬ D(a) Nil I(a) ¬ R(x)  L(x) ¬ D(y)  L(y) D(a) 归结得： (6)R(a) [(5), (4),{a/z}] (7)L(a) [(6), (1),{a/x}] (8)¬D(a) [(7), (2),{a/y}] (9)Nil [(8), (3)] 2019/2/19

5.2.4谓词逻辑中的归结原理(12) 定理5 如果子句集S是不可满足的，那么必存在 一个由S推出空子句的消解序列。 2019/2/19

5.2.4谓词逻辑中的归结原理(13) 练习 设已知： （1）自然数都是大于零的整数； （2）所有整数不是偶数就是奇数； 练习 设已知： （1）自然数都是大于零的整数； （2）所有整数不是偶数就是奇数； （3）偶数除以2是整数。 试证明：所有自然数不是奇数就是其一半为整数的数。 证 首先定义如下谓词： N(x):x是自然数。 I(x):x是整数。 E(x):x是偶数。 O(x):x是奇数。 GZ(x):x大于零。 s(x):x除以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))) 2019/2/19

5.2.4谓词逻辑中的归结原理(14) 利用归结反演法，先证明F1  F2  F3  ¬G是不可满足的。F1  F2  F3  ¬G的子句集为 （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） ¬O(a) （7） ¬I(s(a)) 2019/2/19

5.3应用归结原理求取问题答案(1) 例5.23 已知： （1）如果x和y是同班同学，则x的老师也是y的老师。 （2）王先生是小李的老师。 例5.23 已知： （1）如果x和y是同班同学，则x的老师也是y的老师。 （2）王先生是小李的老师。 （3）小李和小张是同班同学。 问：小张的老师是谁？ 解 首先定义如下谓词： T(x,y)表示x是y的老师 C(x,y)表示x与y是同班同学。 已知条件可以表示成如下谓词公式： F1： x yz(C(x,y)  T(z,x) T(z,y)) F2: T(Wang,Li) F3: C(Li,Zhang) 2019/2/19

5.3应用归结原理求取问题答案(2) 即证明： G： xT(x,Zhang) 为了得到答案，首先要先证明小张的老师是存在的。 即证明： G： xT(x,Zhang) 求F1  F2  F3 ¬ G的子句集： F1： x yz(C(x,y)  T(z,x) T(z,y)) F2: T(Wang,Li) F3: C(Li,Zhang) (1) ¬C(x,y)  ¬T(z,x)  T(z,y) (2)T(Wang,Li) (3)C(Li,Zhang) (4) ¬T(u,Zhang) 2019/2/19

5.3应用归结原理求取问题答案(3) (2)T(Wang,Li) (3)C(Li,Zhang) (4) ¬T(u,Zhang) 归结演绎得： (1) ¬C(x,y)  ¬T(z,x)  T(z,y) (2)T(Wang,Li) (3)C(Li,Zhang) (4) ¬T(u,Zhang) 归结演绎得： (5) ¬C(Li,y)  T(Wang,y) [(1),(2),{Wang/z,Li/x}] (6) ¬C(Li,Zhang) [(4),(5),{Wang/u,Zhang/y}] (7)Nil [(3),(6)] 这说明小张的老师确实是存在的。 2019/2/19

5.3应用归结原理求取问题答案(4) 原来的子句集变为： (1) ¬C(x,y)  ¬T(z,x)  T(z,y) 为了求取答案，给原来的子句增加一个辅助谓词ANS（u）， 得到： (4)' ¬T(u,Zhang)  ANS（u） 原来的子句集变为： (1) ¬C(x,y)  ¬T(z,x)  T(z,y) (2)T(Zhang,Li) (3)C(Li,Zhang) (4)' ¬T(u,Zhang)  ANS（u） 重新归结演绎得： (5) ' ¬C(Li,y)  T(Wang,y) [(1),(2),{Wang/z,Li/x}] (6) ' ¬C(Li,Zhang)  ANS（u） [(4) ',(5) ',{Wang/u,Zhang/y}] (7) ' ANS（Wang） [(3),(6) '] 这说明小张的老师存在且求得小张的老师是王先生。 2019/2/19

5.3应用归结原理求取问题答案(5) 应用归结原理求取问题答案（方法思路） （1）先为待求解的问题找一个合适的求证目标谓词； （2）再增配（以析取形式）一个辅助谓词，该谓词的变元必须与对应目标谓词中的变元完全一致； （3）进行归结； （4）当归结是刚好只剩下辅助谓词时，辅助谓词中原变元位置上的项就是所求的结果。 说明： 其中辅助谓词是一个形式谓词，其作用仅是提取问题的答案。有时就用需求证的目标谓词。 2019/2/19

5.3应用归结原理求取问题答案(6) 例5.24 已知：（1）如果x是y的父亲，y又是z的父亲，则x是z的祖父。 （2）老李是大李的父亲。 （3）大李是小李父亲。 问：上述人员谁和谁是祖孙关系？ 解 首先定义如下谓词： G(x,y)表示x是y的祖父。 F(x,y)表示x与y是父亲。 已知条件可以表示成如下谓词公式： F1： x yz(F(x,y)  F(y,z) G(x,z)) F2: F(Lao,Da) F3: F(Da,Xiao) 2019/2/19

5.3应用归结原理求取问题答案(7) F1： x yz(F(x,y)  F(y,z) G(x,z)) 已知条件可以表示成如下谓词公式： F1： x yz(F(x,y)  F(y,z) G(x,z)) F2: F(Lao,Da) F3: F(Da,Xiao) 并求其子句集如下： (1) ¬ F(x,y)  ¬ F(y,z)  G(x,z) (2) F(Lao,Da) (3)F(Da,Xiao) 设求证的公式为： G： x yG(x,y) (既存在x和y,x是y的祖父) 把其否定化为子句形式再析取一个辅助谓词GA(u，v) (4) ¬ G(u，v)  GA(u，v) 2019/2/19

5.3应用归结原理求取问题答案(8) (1) ¬ F(x,y)  ¬ F(y,z)  G(x,z) (2) F(Lao,Da) 把其否定化为子句形式再析取一个辅助谓词GA(u，v) (1) ¬ F(x,y)  ¬ F(y,z)  G(x,z) (2) F(Lao,Da) (3) F(Da,Xiao) (4) ¬ G(u，v)  GA(u，v) 对上式进行归结： (5) ¬ F(Da，z) G (Lao，z) [(1),(2),{Lao/x,Da/y}] (6) G(Lao，Xiao) [(3),(5),{Xiao/x}] (7) GA(Lao,Xiao) [(4),(6),{Lao/u,Xiao/v}] 所以上述人员中，老李是小李的祖父。 2019/2/19

5.3应用归结原理求取问题答案(9) 练习1：已知如下事实： （1）小李只喜欢较容易的课程； （2）工程类课程是较难的； （3）PR系的所有课程都是较容易的。 （4）PR150是PR系的一门课程 应用归结演绎推理回答问题：小李喜欢什么课程？ 2019/2/19

5.3应用归结原理求取问题答案(10) 练习2：设A、B、C中有人从来不说真话，也有人从来不说谎话，某人向这三人分别同时提出一个问题：谁是说谎者？A答：“B和C都是说谎者”；B答：“A和C都是说谎者”；C答：“A和B中至少有一个人说谎”。用归结原理求谁是老实人，谁是说谎者？ 2019/2/19

5.4归结策略 5.4.1 问题的提出 5.4.2 几种常用的归结策略 5.4.3 归结策略的类型 2019/2/19

5.4.1问题的提出（1） 研究归结原理的目的是实现机器推理 用归结原理实现机器推理的一般性算法 Step3中子句对进行归结的顺序怎么确定 Step1 将子句集S置入CLAUSES表中； Step2 若空子句NIL在CLAUSES中，则归结成功，结 束。 Step3 若CLAUSES表中存在可归结的子句对，则归结 之，并将归结式并入CLAUSES表中，转Step2； Step4 归结失败，退出。 Step3中子句对进行归结的顺序怎么确定 最简单的方法是采用穷举式地进行归结。 2019/2/19

5.4.1问题的提出（2） 水平浸透法具体作法 第一轮 归结先让CLAUSES表（原子句集S）中的子句两两见面 CLAUSES中，得到CLAUSES= S ∪ S1 ； 下一轮 归结让新的CLAUSES表（ S ∪ S1 ）中的子句与S1中 的子句互相见面进行归结，并把产生的归结式集合记为 S2，再将S2并入CLAUSES中； 再一轮 归结时，又让S ∪ S1 ∪ S2与S2中的子句进行归结…… 如此进行，知道某一个Sk中出现空子句为止。 2019/2/19

5.4.1问题的提出（3） S：（1）P  Q （2） ¬ P  Q （3）P  ¬ Q （4） ¬ P  ¬ Q S1：（5）Q [(1),(2)] （6） P [(1),(3)] （7）Q  ¬ Q [(1),(4)] （8） ¬ P  P [(1),(4)] （9）Q  ¬ Q [(2),(3)] （10） ¬ P  P [(2),(3)] （11） ¬ P [(2),(4)] （12）¬ Q [(3),(4)] 2019/2/19

5.4.1问题的提出（4） （25） P [(3),(5)] （26） P  ¬ Q [(3),(7)] （39） NIL [(5),(12)] 2019/2/19

5.4.1问题的提出（5） 控制策略所解决的问题 控制策略的目的 归结点尽量的少。 控制策略的原则 归结过程中中间子句的爆炸。 给出控制策略，以使仅对选择合适的子句间方可做归 结。避免多余的、不必要的归结式出现。或者说，少 做些归结仍能导出空子句。 2019/2/19

5.4.2几种常用的归结策略（1） 删除策略 支持集策略 线性归结策略 输入归结策略 单元归结策略 祖先过滤型策略 2019/2/19

5.4.2几种常用的归结策略（2） 删除策略 类含 若C1，C2是两个子句，若存在替换θ，使得 C1 θ C2，则称子句C1类含C2。 例如：P（x）类含P（a）  Q（y）（只需取θ ＝{a/x}） Q（x）类含P（x）  Q（y）（取θ ＝ε） P（a，x）  P（y，b）类含P（a，b)（取θ ＝ {a/x,b/y} ） 2019/2/19

5.4.2几种常用的归结策略（3） 删除策略 在归结过程中删除以下子句： （1）含有纯文字（子句集中无补的文字）的子句； （2）含有永真式的子句； （3）被子句集中别的子句类含的子句。 2019/2/19

5.4.2几种常用的归结策略（4） 例5.26 S：（1）P  Q （2） ¬ P  Q （3）P  ¬ Q （9）NIL [(5),(8)] 2019/2/19

5.4.2几种常用的归结策略（5） 例5.27 对以下子句集S，用宽度优先策略与删除策略归结。 S： (1) P(x)  Q(x)  ¬R(x) (2) ¬ Q(a) (3) ¬R(a)  Q(a) (4) P(y) (5) ¬P(z)  R(z) （4）类含（1），所以将（1）删除，对其它子句进行归结， S1： (6) ¬ R(a) [(2),(3)] (7) ¬P(a)  Q(a) [(3),(5),{a/z}] (8) R(z) [(4),(5),{z/y}] （6）类含（3），所以将（3）删除 （8）类含（5），所以将（5）删除 第二轮归结在（2）（4）（6）（7）（8）间进行。 2019/2/19

5.4.2几种常用的归结策略（6） (4) P(y) (6) ¬ R(a) (7) ¬P(a)  Q(a) (8) R(z) 在上述子句中进行归结 S2： (9) ¬ P(a) [(2),(7)] (10) Q(a) [(4),(7),{a/y}] (12) NIL [(6),(8),{a/y}] 2019/2/19

5.4.2几种常用的归结策略（7） 删除策略的特点 归结策略的完备性 删除策略的思想是及早删除无用子句，以避免无效归结，缩小搜索规模；并尽量使归结式朝“小”的方向发展。从而尽早导出空子句。 删除策略是完备的。即对于不可满足的子句集，使用删除策略进行归结，最终必导出空子句。 归结策略的完备性 定义2 一个归结策略是完备的，如果对于不可满足的子句集，使用该策略进行归结，最终必导出空子句NIL。 2019/2/19

5.4.2几种常用的归结策略（8） 支持集策略 特点 每次归结时，两个亲本子句中至少要有一个是目标公式否定的子句或其后裔。 目标公式否定的子句集即为支持集。 特点 尽量避免在可满足的子句集中做归结，因为从中导不出空子句。而求证公式的前提通常是一致的，所以支持集策略要求归结时从目标公式否定的子句出发进行归结。支持集策略实际是一种目标制导的反向推理。 支持集策略是完备的。 2019/2/19

5.4.2几种常用的归结策略（9） 例5.28 设有子句集 S： (1) ¬ I(x)  R(x)（为目标公式否定的子句） 例5.28 设有子句集 S： (1) ¬ I(x)  R(x)（为目标公式否定的子句） (2) I(a) (3) ¬R(y)  ¬ L(y) (4) L(a) 我们用支持集策略归结如下： S1： (5) R(a) [(1),(2),{a/x}] (6) ¬ I(x)  L(x) [(1),(3),{x/y}] S2： (7) ¬ L(a) [(5),(3),{a/y}] (8) ¬ L(a) [(6),(2),{a/x}] (9) ¬I(a) [(6),(4),{a/x}] （10）NIL [(7),(4)] 2019/2/19

5.4.2几种常用的归结策略（10） 线性归结策略 特点 线性归结策略归结演绎树 在归结过程中，除第一次归结都用给定的子句集中的子句外，其后每次归结则至少要有一个亲本子句是上次归结的结果。 特点 线性归结策略是完备的，高效的。 可与许多别的策略相兼容。 线性归结策略归结演绎树 Bn－1 Nil C0 C1 … Cn－1 B0 B1 2019/2/19

5.4.2几种常用的归结策略（11） 例5.29 设有子句集 S： (1) ¬ I(x)  R(x)（为目标公式否定的子句） (2) I(a) (3) ¬R(y)  ¬ L(y) (4) L(a) 我们用线性归结策略归结如下： S1： (5) R(a) [(1),(2),{a/x}] (6) ¬ L(a) [(5),(3),{a/y}] （7）NIL [(6),(4)] I(a) R(a) ¬ L(a) Nil ¬ R(x)  I(x) ¬ R(y)  ¬ L(y) L(a) 2019/2/19

5.4.2几种常用的归结策略（12） 输入归结策略 特点 每次参加归结的两个亲本子句，必须至少有个一是初始子句集中的子句。 是一种自底而上的归结策略。 输入归结策略是不完备的。 输入归结策略常同线性归结策略结合，构成线性输入归结策略。 也可以与支持集策略相结合。 2019/2/19

5.4.2几种常用的归结策略（13） 单元归结策略 特点 单元优先策略 在归结过程中，每次参加归结的两个亲本子句中必须至少有一个为单元子句。 单元归结的思想是用单元子句归结可以使归结式含有较少的文字，因而有利于逼近空子句。 单元归结策略是不完备的，但效率高。 单元优先策略 将单元归结策略的条件放宽，优先对单元子句进行归结。 2019/2/19

5.4.2几种常用的归结策略（14） 祖先过滤形策略 特点 参加归结的两个子句，要么至少有一个是初始子句集中的子句，要么一个是另一个的祖先。 是线性输入策略的改进。 是完备的。 2019/2/19

5.4.2几种常用的归结策略（15） 例5.30 设有子句集 S＝{¬ P(x)  Q(x), ¬ P(x)  ¬ Q(x)， P(u)  Q(u)， P(t)  ¬ Q(t)} ¬ P(x)  Q(x) ¬ P（x） P(u)  Q(u) Nil ¬ P(x)  ¬ Q(x) P(t)  ¬ Q(t) ¬ Q(x) P（x） 2019/2/19

5.4.3归结策略的类型（1） 常用的归结策略 锁归结策略 语义归结策略 加权策略 用数字对子句中的文字进行编号，这种编号就称为文字的锁。在归结过程中，参加归结的文字必须分别是所在子句中编号最小者。 语义归结策略 将子句集S中子句分为两组，只考虑组间子句的归结。 加权策略 对子句或其中的项赋以权值，归结用权值来控制 2019/2/19

5.4.3归结策略的类型（2） 归结策略的类型 简化性策略 限制型策略 有序性策略 尽量简化子句和子句集，避免无效归结。 删除策略。 尽量缩小搜索范围，提高搜索效率。 支持集策略、线性策略、输入策略、单元策略、祖先过滤策略、语义归结。 有序性策略 给子句安排一定顺序，尽快推出空子句。 单元优先策略、加权策略、锁归结策略。 2019/2/19

5.4.3归结策略的类型（3） 用归结策略实现机器推理的一般性算法 Step2 若空子句NIL在CLAUSES中，则归结成功，结束。 Step1 将子句集S置入CLAUSES表中； Step2 若空子句NIL在CLAUSES中，则归结成功，结束。 Step3 按某种策略在CLAUSES表中寻找可归结的子句对，若存在则归结之，并将归结式并入CLAUSES表中，转Step2； Step4 归结失败，退出。 2019/2/19

5.6Horn子句归结与逻辑程序 5.6.1 子句的蕴含表示形式 5.6.2 Horn子句与逻辑程序 补充 浅识Prolog 2019/2/19

5.6.1子句的蕴含表示形式(1) 任何子句总可以表示成如下形式（Pi， Qj皆为文字）： 式（1）可以进一步变形为： 约定蕴含式前件文字恒为合取关系，后件恒为析取关系，式（2） 又可以改写为： 特殊情形，当n＝0时，（4）式可以表示为： 特殊情形，当m＝0时，（4）式可以表示为： 式（3）又可以变形为（4），（4）也被称为子句的蕴含表达式： 2019/2/19

5.6.1子句的蕴含表示形式(2) 例 （1）从其中一个子句的“ ”号左侧与另一个子句的“ ”号右侧的文字中寻找可合一文字对； （1）从其中一个子句的“ ”号左侧与另一个子句的“ ”号右侧的文字中寻找可合一文字对； （2）然后消去可合一文字对；并把其余的左部（即“ ”号的左侧）文字合并，作为消解式的左部，其余的右部文字合并，作为消 解式的右部。 2019/2/19

5.6.2Horn子句与逻辑程序(1) Horn子句的定义 定义：至多含有一个正文字的子句称为称为Horn（霍恩）子句。 2019/2/19

5.6.2Horn子句与逻辑程序(2) 例5.31 P（a，c）式下面子句集{(1), (2), (3), (4)}的逻辑结论。 （前提） （目标子句否定式） 从目标子句出发，采用线性归结： 2019/2/19

5.6.2Horn子句与逻辑程序(3) 上述归结过程除最后一次外，每次产生的归结式都是目标子句 归结过程就是对第一个目标的求解导致了一连串目标求解 目标求解过程类似于计算机程序执行中的过程调用 基于Horn子句集的线形归结与程序与程序的执行，二者是不谋而合。 2019/2/19

5.6.2Horn子句与逻辑程序(4) Horn子句逻辑可以作为一种计算机程序语言。每一个Horn子句就是该语言中的语句，一个Horn子句的有限集合就是一个程序。这种用Horn子句组成的程序为逻辑程序。 Prolog语言就是以Horn子句逻辑为基础的程序设计语言。 2019/2/19

5.6.2Horn子句与逻辑程序(5) Prolog程序的运行是一种从问题语句（目标语句）开始的线形归结过程。 每次归结时，子目标的选择顺序是从左到右，新子目标的插入顺序是插入子目标队列的左端，匹配子句的顺序是自上而下，搜索空子句是深度优先，推理方式是反向推理，且有回溯机制。Prolog这种方法成为基于Horn子句的SLD（Linear resolution with Selection function for Definite Clause）归结。 2019/2/19

浅识Prolog（1） likes(bell,sports). likes(mary,music). likes(mary,sports) 例子 likes(bell,sports). likes(mary,music). likes(mary,sports) likes(jane ,smith). friend(john,X):-likes(X,reading),likes(X,music). friend(john,X):-likes(X,sports),likes(X,music). ?-friend(john,Y). 2019/2/19

浅识Prolog（2） PROLOG程序中的目标可以变化，也可以含有多个语句(上例中只有一个)。如果有多个语句，则这些语句称为子目标。 ?-likes(mary,X). 或 ?-likes(mary,music). ?-friend(X,Y). ?-likes(bell,sports), likes(mary,music), friend(john,X). 2019/2/19

浅识Prolog（3） POROLOG程序运行机理是基于归结原理的演绎推理。PROLOG程序的运行是从目标出发，并不断进行匹配、合一、归结，回溯，直到目标被完全满足。 自由变量与约束变量 无值的变量为自由变量。 有值的变量为约束变量。 一个变量取了某值就说该变量约束于某值，或者说该变量被某值所约束，或者说该变量被某值实例化了。 2019/2/19

浅识Prolog（4） 匹配合一 两个谓词可匹配合一，是指两个谓词的名相同，参量项的个数相同，参量类型对应相同，并且对应参量项还满足下列条件之一： 如果两个都是常量，则必须完全相同。 如果两个都是约束变量，则两个约束值必须相同。 如果其中一个是常量，一个是约束变量，则约束值与常量必须相同。 至少有一个是自由变量。 合一操作 两个自由变量 一个自由变量一个常量 2019/2/19

浅识Prolog（5） 例如：下面的两个谓词 pre1("ob1","ob2",Z) pre1("ob1",X,Y) 只有当变量X被约束为"ob2"，且Y、Z的约束值相同或者至少有一个是自由变量时，它们才是匹配合一的。 2019/2/19

浅识Prolog（6） 回溯， 回溯就是在程序运行期间，当某一个子目标不能满足（即谓词匹配失败）时，控制就返回到前一个已经满足的子目标（如果存在的话），并撤消其有关变量的约束值，然后再使其重新满足。 成功后，再继续满足原子目标。 如果失败的子目标前再无子目标，则控制就返回到该子目标的上一级目标（即该子目标谓词所在规则的头部）使它重新匹配。 2019/2/19

浅识Prolog（7） 运行过程 likes(bell,sports). likes(mary,music). likes(mary,sports) likes(jane ,smith). friend(john,X):- likes(X,reading),likes(X,music). friend(john,X):-likes(X,sports),likes(X,music). ?-friend(john,Y). 2019/2/19

浅识Prolog（8） 系统对程序进行扫描，寻找能与目标谓词匹配合一的事实或规则头部。规则 friend(john,X):-likes(X,reading),likes(X,music). 的头部可与目标谓词匹配合一，对原目标的求解就转化为对新目标 likes(X,reading),likes(X,music). 的求解。 2019/2/19

浅识Prolog（9） 子目标的求解过程与主目标完全一样，也是从头对程序进行扫描，不断进行测试和匹配合一等，直到匹配成功或扫描完整个程序为止。可以看出，对第一个子目标like(X,reading)的求解因无可匹配的事实和规则而立即失败，进而导致规则 friend(john,X):-likes(X,reading),likes(X,music). 的整体失败。于是，刚才的子目标 likes(X,reading)和likes(X,music) 被撤消，系统又回溯到原目标friend(john,X)。 2019/2/19

浅识Prolog（10） 系统从该目标刚才的匹配语句处（即第五句）向下继续扫描程序中的子句，试图重新使原目标匹配，结果发现第六条语句的左部，即规则 friend(john,X):-likes(X,sports),likes(X,music). 的头部可与目标为谓词匹配。但由于这个语句又是一个规则，于是，这时对原目标的求解，就又转化为依次对子目标 likes(X,sports)和likes(X,music) 的求解。 2019/2/19

浅识Prolog（11） 子目标likes(X,sports)与程序中的事实立即匹配成功，且变量X被约束为bell。于是，系统便接着求解第二个子目标。由于变量X已被约束，所以这时第二个子目标实际上已变成了 likes(bell,music). 由于程序中不存在事实likes(bell,music)，所以该目标的求解失败。 2019/2/19

浅识Prolog（12） 系统就放弃这个子目标，并使变量X恢复为自由变量，然后回溯到第一个子目标，重新对它进行求解。由于系统已经记住了刚才已同第一子目标谓词匹配过的事实的位置，所以重新求解时，便从下一个事实开始测试。 易见，当测试到程序中第三个事实时，第一个子目标便求解成功，且变量X被约束为mary。这样，第二个子目标也就变成了 likes(mary,music). 再对它进行求解。 2019/2/19

浅识Prolog（13） 由于两个子目标都求解成功，所以，原目标friend(john,Y)也成功，且变量Y被约束为mary(由Y与X的合一关系)。于是，系统回答： Y=mary 程序运行结束。 2019/2/19

浅识Prolog（14） likes(bell,sports). likes(mary,music). likes(mary,sports) likes(jane ,smith). friend(john,X):- likes(X,reading),likes(X,music). likes(X,sports),likes(X,music). ?-friend(john,Y). 浅识Prolog（14） 2019/2/19

5.7非归结演绎推理(1) Bledsoe自然演绎法 基于规则的演绎推理 王浩算法 这种方法采用多条推理规则，试图模拟人脑的推理证明方式，由前提推证结论。 基于规则的演绎推理 这种推理将前提谓词公式集合分为规则和事实两部分，并以特定的形式加以表示，然后用规则与事实进行匹配，进行演绎推理。基于规则的演绎推理系统，称为规则演绎系统。 王浩算法 这是一种利用公理系统进行机械化自动定理证明的方法。它完全脱离人的经验和技巧，机械地构造推理步骤，证明一个命题逻辑定理成立。这个系统是完备的。 2019/2/19

编程实践 求谓词公式的子句集； 命题逻辑的归结演绎推理系统； 求谓词公式的MGU； 谓词公式的合一运算； 谓词逻辑的归结演绎推理系统/问题求解； 根据受限的自然语言描述自动生成谓词公式； 依据删除策略的命题归结演绎推理系统； 依据支持集策略的命题归结演绎推理系统； 依据线形策略的命题归结演绎推理系统； Horn子句的归结推理系统。 2019/2/19

The End！ 2019/2/19