第三章基于谓词逻辑的机器推理--32归结 演绎推理 321子句集 定义1原子谓词公式及其否定称为文字;文字的析取式 称为子句;r个文字组成的子句称为r文字子句。1-文 字子句也称为单元子句。不含任何文字的子句称为空 子句,记为或ML。由子句构成的集合称为子句集。 任何一个谓词公式都可以化为子句集,步骤如下: (1)、利用等价式A→B分AVB 和A分>B令(A→>B)∧(B→A)消去联结词“→”和 (2)、缩小否定联结词的作用范围,使其仅作用于 原子公式。可利用下列等价式:
第三章 基于谓词逻辑的机器推理----3.2 归结 演绎推理 3.2.1子句集 定义1 原子谓词公式及其否定称为文字；文字的析取式 称为子句；r个文字组成的子句称为r-文字子句。1-文 字子句也称为单元子句。不含任何文字的子句称为空 子句，记为•或NIL。由子句构成的集合称为子句集。 任何一个谓词公式都可以化为子句集，步骤如下： （1）、利用等价式A → B A B 和 A B (A → B) (B → A)消去联结词“ → ” 和 “ ”。 （2）、缩小否定联结词的作用范围，使其仅作用于 原子公式。可利用下列等价式：
GAbA (AVB)今=A∧=B; (A入B)_AyB; XA(x)彐xA(x); 彐xA(x)分Vx-A(X) (3)、重新命名变元名,使不同量词约束的 变元有不同的名字
A A； (AB) A B； (A B) A B； xA(x) x A(x)； xA(x) x A(x) （3）、重新命名变元名，使不同量词约束的 变元有不同的名字
(4)、消去存在量词。若存在量词不在全称量 词的辖域内,则用一个常量符号替换该存在量 词辖域中的相应约束变元。这样的常量称为 Skolem常量;若该存在量词在一个或多个全称 量词的辖域内,则用这些全称量词指导变元的 个函数替换该存在量词约束的变元。这样的 函数称为 Skolem函数。 例如∨x1Vx2xn3yP(x1x2,xny)中y可用 Skolem函数f ,xn)替换为x1Vx2 VX,P(XI xn, f(x1,x,,.,n)
（4）、消去存在量词。若存在量词不在全称量 词的辖域内，则用一个常量符号替换该存在量 词辖域中的相应约束变元。这样的常量称为 Skolem常量；若该存在量词在一个或多个全称 量词的辖域内，则用这些全称量词指导变元的 一个函数替换该存在量词约束的变元。这样的 函数称为Skolem函数。 例如x1 x2 • • •xnyP(x1 ,x2 ,…, xn ,y)中y可用 Skolem函数f(x1 ,x2 ,…, xn )替换为x1 x2 • • • xnP(x1 ,x2 ,…, xn ,f(x1 ,x2 ,…, xn ))
(5)、把全称量词全部移到公式的左边 (6)、把全称量词后面的公式利用等价关系 Av(BAC)分(AVB)∧(AVC)化为子句的合取 式,得到的公式称为 Skolem标准形。 Skolem 标准形的一般形式为Vx1Yx2xnM,其中 M是子句的合取式。 (7)、消去全称量词。 (8)、对变元更名,使子句间无同名变元
（5）、把全称量词全部移到公式的左边。 （6）、把全称量词后面的公式利用等价关系 A(B C) (AB) (A C)化为子句的合取 式，得到的公式称为Skolem标准形。Skolem 标准形的一般形式为x1 x2 • • •xnM，其中 M是子句的合取式。 （7）、消去全称量词。 （8）、对变元更名，使子句间无同名变元
(9)、消去合取词入,以子句为元素组成的 集合称为谓词公式的子句集 例、把谓词公式∨x{yP(xy)→> √yQ(xy))R(xy)化为子句集。 定理1谓词公式G不可满足当且仅当其子句 集S不可满足。子句集S是不可满足的是指其 全部子句的合取式是不可满足的
（9）、消去合取词 ，以子句为元素组成的 集合称为谓词公式的子句集。 例、把谓词公式x{yP(x,y) → y[Q(x,y)→R(x,y)]}化为子句集。 定理1 谓词公式G 不可满足当且仅当其子句 集S不可满足。子句集S是不可满足的是指其 全部子句的合取式是不可满足的
3.2.2命题逻辑中的归结原理 ◆要证明在前提P下结论Q成立,即是证明P→Q永真, 这只须证明P∧_Q不可满足。根据定理1,只须证 明P∧Q的子句集不可满足。由于子句之间是合取 关系,只要有一个子句不可满足,则整个子句集不 可满足。由于空子句是不可满足的,所以如果子句一 集中包含空子句,则该子句集是不可满足的。若子 句集中不包含空子句,则可通过 Robinson提出的归 结原理对子句集进行归结,归结过程保证子句集的 不可满足性不变。一旦归结出空子句,则证明结束 因此,归结原理把定理的证明化为子句集中归结出 空子句的过程
3.2.2 命题逻辑中的归结原理 要证明在前提P下结论Q成立，即是证明P → Q永真， 这只须证明P Q不可满足。根据定理1，只须证 明P Q的子句集不可满足。由于子句之间是合取 关系，只要有一个子句不可满足，则整个子句集不 可满足。由于空子句是不可满足的，所以如果子句 集中包含空子句，则该子句集是不可满足的。若子 句集中不包含空子句，则可通过Robinson提出的归 结原理对子句集进行归结，归结过程保证子句集的 不可满足性不变。一旦归结出空子句，则证明结束。 因此，归结原理把定理的证明化为子句集中归结出 空子句的过程
定义4、设L是一个文字,则称L与为互补 文字。 定义5、设C1、C2是命题逻辑中的两个子句, C1中有文字L1,C2中有文字L2,且L1与L2 互补,从C1,C2中分别删除L1,L2,再将剩 余部分析取起来,构成的新子句C12称为C1与 C2的归结式(消解式),C1,C2称为C12的亲 本子句
定义４、设L是一个文字，则称L与L为互补 文字。 定义５、设C1、C2是命题逻辑中的两个子句， C1 中有文字L1 ， C２ 中有文字L２，且L1与L２ 互补， 从C1，C２中分别删除L1 ， L２，再将剩 余部分析取起来，构成的新子句C1２称为C1与 C2的归结式（消解式）， C1，C2称为C1２的亲 本子句
定理2、归结式C12是其亲本子句C1与C2 的逻辑结论 ※推论、设C1,C2是子句集S的两个子句, C12是它们的归结式,则 (1)若用C12代替C1和C2后得到新子 句集S1,则由S1的不可满足性可推出原 子句集S的不可满足性。即 S1不可满足→S不可满足
定理２、归结式C1２是其亲本子句C1与C2 的逻辑结论。 推论、设C1，C2是子句集S的两个子句， C1２是它们的归结式，则 （１）若用C1２代替C1和C2后得到新子 句集S1，则由S1的不可满足性可推出原 子句集S的不可满足性。即 S1不可满足S不可满足
(2)若把C12加入到S中,得到新子句集 S2,则S2与S在不可满足意义上是等价 的。即 S2不可满足◇S不可满足 例、用归结原理证明R是P,(P∧Q) →R,(SVU)→R,U的逻辑结 果
（２）若把C1２加入到S中，得到新子句集 S２，则S２与S在不可满足意义上是等价 的。即 S2不可满足 S不可满足 例、用归结原理证明R是P， （P Q） → R， （ SU） → R，U的逻辑结 果
3.2.3替换与合 定义6、一个替换( Substitution是形如{t1/x1 t2/x2…,n/xn}的有限集合,其中t,t2,…,tn 是项,x1,x2,,xn是互不相同的个体变元。 七/x表示用t代换x1。t与x不同,x也不能出 现在中(=1,2,n 例、(ax,g(y)y,fg(b)/z}是一个替换, g(y)x,fx)y}不是一个替换
3.2.3 替换与合一 定义６、一个替换(Substitution)是形如{t1 / x1 , t2 / x2 ,…,tn / xn }的有限集合，其中t1 , t2 ,…,tn 是项， x1 , x2 ,…,xn是互不相同的个体变元。 t i / xi表示用t i代换xi 。 t i与xi不同，xi也不能出 现在t j中(j=1,2,…,n)。 例、｛a/x, g(y)/y, f(g(b))/z}是一个替换， {g(y)/x, f(x)/y}不是一个替换