《人工智能原理教案02章归结推理方法2.3谓词逻辑归结法基精》由会员分享，可在线阅读，更多相关《人工智能原理教案02章归结推理方法2.3谓词逻辑归结法基精（8页珍藏版）》请在金锄头文库上搜索。
1、2.3谓词逻辑归结法基础由于谓词逻辑与命题逻辑不同，有量词、变量和函数，所以 在生成子句集之前要对逻辑公式做处理，具体的说就是要将其转 化为Skolem标准形，然后在子句集的基础上再进行归结，虽然基 本的归结的基本方法都相同，但是其过程较之命题公式的归结过 程要复杂得多。本节针对谓词逻辑归结法介绍了Skolem标准形、子句集等一些必要的概念和定理。2. 3. 1 Skolem 标准形Skolem标准形的定义：前束范式中消去所有的存在量词，则称这种形式的谓词公式 为Skolem标准形，任何一个谓词公式都可以化为与之对应的 Skolem标准形。但是，Skolem标准形不唯一。前束范式：A是一个前束
2、范式，如果 A中的一切量词都位于 该公式的最左边(不含否定词)，且这些量词的辖域都延伸到公 式的末端。Skolem标准形的转化过程为，依据约束变量换名规则，首先 把公式变型为前束范式，然后依照量词消去原则消去或者略去所 有量词。具体步骤如下：将谓词公式G转换成为前束范式前束范式的形式为：(Q1x1(Q2x2(QnxnM(x1,x2,xn即：把所有的量词都提到前面去。注意：由于所有的量词的辖域都延伸到公式的末端，即，最 左边量词将约束表达式中的所有同名变量。所以将量词提到公式 最前端时存在约束变量换名问题。要严守规则。约束变量换名规则:（Qx M（ x）二（Qy） M（ y）（Qx M （x,z
3、）（Qy） M （y,z）量词否定等值式：（Hx M （x）吕（弓y ）M （y）（ M （x）台（飞 y ）M （y）量词分配等值式：c x ( P (x) A Q (x)= C x P (x)(x ( P (x) V Q (x) U (Tx P (x) V x Q (x)消去量词等值式：设个体域为有穷集合（a1, a2,anA A P (an )V V P (an)c x P (x) HP (a1) A P (a2)(x P (x) =P (a1) V P (a2)量词辖域收缩与扩张等值式:c x ( P (x) V Q 一(x P (x) V Qc x ( P (x) A Q x P (
4、x) A Q(0x ( P (x) Q Vx P(x)QC x ( Q (x)Q ( x P(x)(長(P (x)V Q 台( P(x)VQ(長(P (x)A Q =&x P(x)AQ(長(P (x) Q 吕(Vx P(x)Q(ilx ( Q P( x) =Q (3 x P (x )消去量词量词消去原则：1消去存在量词”，即，将该量词约束的变量用任意常量a, b等)、或全称变量的函数(f(x, g(y等代替。如果存在量词左 边没有任何全称量词，则只将其改写成为常量；如果是左边有全 程量词的存在量词，消去时该变量改写成为全程量词的函数。2略去全程量词，简单地省略掉该量词。Skolem 定理：谓词
5、逻辑的任意公式都可以化为与之等价的前束范式，但其 前束范式不唯一。注意：公式G的SKOLEM标准形同G并不等值。例题2-2将下式化为Skolem标准形:( x(yP(a, x, yX(C yQ(y, b f R(x解：第一步，消去f号，得:(E x(弓 yP(a, x, y V (Tx (飞 yQ(y, b V R(x第二步，深入到量词内部，得：x( _ yP(a, x, y 人(_ x ( yQ(y, b V R(x=(x( 一 yP(a, x, y A ( x (y Q(y, b 人R(x第三步，全称量词左移，(利用分配律)，得C x( (一 yP(a, x, y A ( _ y(Q(y,
6、 b A R(x第四步，变元易名，存在量词左移，直至所有的量词移到前 面，得：C x(二 yP(a, x, y A (二 y(Q(y, b A R(x=(x (yP(a, x, y A ( z(Q(z, bA R(x=(H x (司 y (司 z (P(a, x, y A Q(z, b A R(x由此得到前述范式第五步，消去(存在量词)，略去一全称量词消去Gy，因为它左边只有(x，所以使用x的函数f(x代替 之，这样得到：(x(二 z( P(a, x, f(x 人Q(z, b 人R(x消去Vz,同理使用g(x代替之，这样得到：(x ( P(a, x, f(x 人Q(g(x, b 人R(x贝U,
7、略去全称变量，原式的 Skolem标准形为：P(a, x, f(x 人Q(g(x, b 人R(x232子句集文字：不含任何连接词的谓词公式。子句：一些文字的析取(谓词的和)。子句集：所有子句的集合对于任一个公式 G,都可以通过Skolem标准形，标准化建立起一 个子句集与之相对应。因为子句不过是一些文字的析取，是一种 比较简单的形式，所以对 G的讨论就用对子句集 S的讨论来代 替，以便容易处理。子句集S可由下面的步骤求取：1.谓词公式G转换成前束范式2消去前束范式中的存在变量，略去其中的任意变量，生成SKOLEMB 准形3将SKOLEMB准形中的各个子句提出，表示为集合形式教师提示：为了简单起
8、见，子句集生成可以理解为是用,取代SKOLEMB准形中的A ,并表示为集合形式 。注意：SKOLEN标准形必须满足合取范式的条件。即，在生成 子句集之前逻辑表达式必须是各 谓词表达式或谓词或表达式 的与。定理谓词表达式G是不可满足的当且仅当 其子句集S是不可满足 的公式G与其子句集S并不等值，但它们在不可满足的意义下是一 致的。因此如果要证明 A1A A2 A AB，只需证明G= A1A A2 A A3 AB的子句集是不可满足的，这也正是引入子句集 的目的。注意：公式G和子句集S虽然不等值，但是它们的之间一般 逻辑关系可以简单的说明为：G真不一定S真，而S真必有G真，即，S 在生成SKOLEN
9、标准形时将存在量词用常量或其他变 量的函数代替，使得变量讨论的论域发生了变化，即论域变小 了。所以G不能保证S真。定理的推广对于形如G = G1 A Q A G3 AA G的谓词公式，G的子句 集的求取过程可以分解成几个部分单独处理。如果 Gi的子句集为 Si，则有S = S1 U S2 U S3 UU Sn，虽然G的子句集不为 S, 但是可以证明：SG与S1 U S2 U S3 UU Sn在不可满足的意义上是一致的。即SG不可满足S1 U S2 U S3 UU Sn不可满足 由上面的定理，我们对 SG的讨论，可以用较为简单的 S1 U S2 U S3 UU Sn来代替。为方便起见，也称 S1
10、 U S2 U S3 UU Sn为G的子句形，即：SG= S1 U S2 U S3 UU Sn。根据以上定理可对一个谓词表达式分而治之，化整为零，大大减少了计算复杂度。例2-3对所有的x,y,z来说，如果y是x的父亲，z又是y的父亲， 则z是x的祖父。又知每个人都有父亲，试问对某个人来说谁是 它的祖父？用一阶逻辑表示这个问题，并建立子句集。解：这里我们首先引入谓词：P(x, y表示x是y的父亲Q(x, y表示x是y的祖父ANS(x表示问题的解答于是有：对于第一个条件，如果y是x的父亲，z又是y的父亲，则z 是x的祖父，一阶逻辑表达式如下：A1 : C x( y( z(P(x, y A P(y, z Q(x, z则把A1化为合取范式，进而化为 Skolem标准形，表示如下:S A1:P(x ,y V P(y, z V Q(x, z对于第一个条件：每个人都有父亲，一阶逻辑表达式如下：A2 :y(二 xP(x, y化为Skolem标准形，表示如下：S A2: P(f(y, x结论：某个人是它的祖父B：(x(yQ(x, y否定后得到子句：SB :Q(x, y V ANS(x则得到的相应的子句集为： S A1 , S A2 , SB 解毕。
