人工智能原理教案02章归结推理方法23谓词逻辑归结法基(精).docVIP

人工智能原理教案02章归结推理方法23谓词逻辑归结法基(精)

2.3谓词逻辑归结法基础

由于谓词逻辑与命题逻辑不同，有量词、变量和函数，所以在生成子句集之前要对逻辑公式做处理，具体的说就是要将其转化为Skolem标准形，然后在子句集的基础上再进行归结，虽然基本的归结的基本方法都相同，但是其过程较之命题公式的归结过程要复杂得多。

本节针对谓词逻辑归结法介绍了Skolem标准形、子句集等一些必要的概念和定理。

2．3．1Skolem标准形

Skolem标准形的定义：

前束范式中消去所有的存在量词，则称这种形式的谓词公式为Skolem标准形，任何一个谓词公式都可以化为与之对应的Skolem标准形。但是，Skolem标准形不唯一。

前束范式：A是一个前束范式，如果A中的一切量词都位于该公式的最左边（不含否定词），且这些量词的辖域都延伸到公式的末端。

Skolem标准形的转化过程为，依据约束变量换名规则，首先把公式变型为前束范式，然后依照量词消去原则消去或者略去所有量词。具体步骤如下：

将谓词公式G转换成为前束范式

前束范式的形式为：

(Q1x1(Q2x2…(QnxnM(x1,x2,…,xn

即：把所有的量词都提到前面去。

注意：由于所有的量词的辖域都延伸到公式的末端，即，最左边量词将约束表达式中的所有同名变量。所以将量词提到公式最前端时存在约束变量换名问题。要严守规则。

约束变量换名规则：

(QxM（x）（Qy）M（y）

(QxM（x,z）（Qy）M（y,z）

量词否定等值式：

～(xM（x）（y）～M（y）

～(xM（x）（y）～M（y）

量词分配等值式：

(x(P（x）∧Q（x）(xP（x）∧(xQ（x）

(x(P（x）∨Q（x）(xP（x）∨(xQ（x）

消去量词等值式：设个体域为有穷集合（a1,a2,…an）

(xP（x）P（a1）∧P（a2）∧…∧P（an）

(xP（x）P（a1）∨P（a2）∨…∨P（an）

量词辖域收缩与扩张等值式：

(x(P（x）∨Q(xP（x）∨Q

(x(P（x）∧Q(xP（x）∧Q

(x(P（x）→Q(xP（x）→Q

(x(Q→P（x）Q→(xP（x）

(x(P（x）∨Q(xP（x）∨Q

(x(P（x）∧Q(xP（x）∧Q

(x(P（x）→Q(xP（x）→Q

(x(Q→P（x）Q→(xP（x）

消去量词

量词消去原则：

1消去存在量词，即，将该量词约束的变量用任意常量（a,b等）、或全称变量的函数(f(x,g(y等代替。如果存在量词左边没有任何全称量词，则只将其改写成为常量；如果是左边有全程量词的存在量词，消去时该变量改写成为全程量词的函数。

2略去全程量词，简单地省略掉该量词。

Skolem定理：

谓词逻辑的任意公式都可以化为与之等价的前束范式，但其前束范式不唯一。

注意：公式G的SKOLEM标准形同G并不等值。

例题2-2

将下式化为Skolem标准形：

～(x(yP(a,x,y→(x(～(yQ(y,b→R(x

解：

第一步，消去→号，得：

～(～(x(yP(a,x,y∨(x(～～(yQ(y,b∨R(x

第二步，～深入到量词内部，得：

(x(yP(a,x,y∧～(x((yQ(y,b∨R(x

＝(x(yP(a,x,y∧(x((y～Q(y,b∧～R(x

第三步，全称量词左移，（利用分配律），得

(x((yP(a,x,y∧(y(～Q(y,b∧～R(x

第四步，变元易名，存在量词左移，直至所有的量词移到前面，得：

(x((yP(a,x,y∧(y(～Q(y,b∧～R(x

＝(x((yP(a,x,y∧(z(～Q(z,b∧～R(x

=(x(y(z(P(a,x,y∧～Q(z,b∧～R(x

的谓词公式，G的子句集的求取过程可以分解成几个部分单独处理。如果Gi的子句集为Si，则

有S=S1∪S2∪S3∪…∪Sn，虽然G的子句集不为S，但是可以证明：

SG与S1∪S2∪S3∪…∪Sn在不可满足的意义上是