第三章基于谓词逻辑的机器推理--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是不可满足的是指其 全部子句的合取式是不可满足的