预览加载中,请您耐心等待几秒...
1/8
2/8
3/8
4/8
5/8
6/8
7/8
8/8

在线预览结束,喜欢就下载吧,查找使用更方便

如果您无法下载资料,请参考说明:

1、部分资料下载需要金币,请确保您的账户上有足够的金币

2、已购买过的文档,再次下载不重复扣费

3、资料包下载后请先用软件解压,在使用对应软件打开

2.3谓词逻辑归结法基础由于谓词逻辑与命题逻辑不同,有量词、变量和函数,所以在生成子句集之前要对逻辑公式做处理,具体的说就是要将其转化为Skolem标准形,然后在子句集的基础上再进行归结,虽然基本的归结的基本方法都相同,但是其过程较之命题公式的归结过程要复杂得多。本节针对谓词逻辑归结法介绍了Skolem标准形、子句集等一些必要的概念和定理。2.3.1Skolem标准形 Skolem标准形的定义:前束范式中消去所有的存在量词,则称这种形式的谓词公式为Skolem标准形,任何一个谓词公式都可以化为与之对应的Skolem标准形。但是,Skolem标准形不唯一。前束范式:A是一个前束范式,如果A中的一切量词都位于该公式的最左边(不含否定词),且这些量词的辖域都延伸到公式的末端。Skolem标准形的转化过程为,依据约束变量换名规则,首先把公式变型为前束范式,然后依照量词消去原则消去或者略去所有量词。具体步骤如下:将谓词公式G转换成为前束范式前束范式的形式为:(Q1x1)(Q2x2)…(Qnxn)M(x1,x2,…,xn)即:把所有的量词都提到前面去。注意:由于所有的量词的辖域都延伸到公式的末端,即,最左边量词将约束表达式中的所有同名变量。所以将量词提到公式最前端时存在约束变量换名问题。要严守规则。约束变量换名规则:(Qx)M(x)(Qy)M(y)(Qx)M(x,z)(Qy)M(y,z)量词否定等值式:~(x)M(x)(y)~M(y)~(x)M(x)(y)~M(y)量词分配等值式:(x)(P(x)∧Q(x))(x)P(x)∧(x)Q(x)(x)(P(x)∨Q(x))(x)P(x)∨(x)Q(x)消去量词等值式:设个体域为有穷集合(a1,a2,…an)(x)P(x)P(a1)∧P(a2)∧…∧P(an)(x)P(x)P(a1)∨P(a2)∨…∨P(an)量词辖域收缩与扩张等值式:(x)(P(x)∨Q)(x)P(x)∨Q(x)(P(x)∧Q)(x)P(x)∧Q(x)(P(x)→Q)(x)P(x)→Q(x)(Q→P(x))Q→(x)P(x)(x)(P(x)∨Q)(x)P(x)∨Q(x)(P(x)∧Q)(x)P(x)∧Q(x)(P(x)→Q)(x)P(x)→Q(x)(Q→P(x))Q→(x)P(x) 消去量词量词消去原则:1)消去存在量词"",即,将该量词约束的变量用任意常量(a,b等)、或全称变量的函数(f(x),g(y)等)代替。如果存在量词左边没有任何全称量词,则只将其改写成为常量;如果是左边有全程量词的存在量词,消去时该变量改写成为全程量词的函数。2)略去全程量词"",简单地省略掉该量词。Skolem定理:谓词逻辑的任意公式都可以化为与之等价的前束范式,但其前束范式不唯一。注意:公式G的SKOLEM标准形同G并不等值。 例题2-2将下式化为Skolem标准形:~(x)(y)P(a,x,y)→(x)(~(y)Q(y,b)→R(x))解:第一步,消去→号,得:~(~(x)(y)P(a,x,y))∨(x)(~~(y)Q(y,b)∨R(x))第二步,~深入到量词内部,得:(x)(y)P(a,x,y)∧~(x)((y)Q(y,b)∨R(x))=(x)(y)P(a,x,y)∧(x)((y)~Q(y,b)∧~R(x))第三步,全称量词左移,(利用分配律),得(x)((y)P(a,x,y)∧(y)(~Q(y,b)∧~R(x)))第四步,变元易名,存在量词左移,直至所有的量词移到前面,得:(x)((y)P(a,x,y)∧(y)(~Q(y,b)∧~R(x)))=(x)((y)P(a,x,y)∧(z)(~Q(z,b)∧~R(x)))=(x)(y)(z)(P(a,x,y)∧~Q(z,b)∧~R(x))由此得到前述范式第五步,消去""(存在量词),略去""全称量词消去(y),因为它左边只有("x),所以使用x的函数f(x)代替之,这样得到:(x)(z)(P(a,x,f(x))∧~Q(z,b)∧~R(x))消去(z),同理使用g(x)代替之,这样得到:(x)(P(a,x,f(x))∧~Q(g(x),b)∧~R(x))则,略去全称变量,原式的Skolem标准形为:P(a,x,f(x))∧~Q(g(x),b)∧~R(x) 2.3.2子句集文字:不含任何连接词的谓词公式。子句:一些文字的析取(谓词的和)。子句集:所有子句的集合 对于任一个公式G,都可以通过Skolem标准形,标准化建立起一个子句集与之相对应。因为子句不过是一些文字的析取,是一种比较简单的形式,所以对G的讨论就用对子句集S的讨论来代替,以便容易处理。子句集S可由下面的步骤求取:1.谓词公式G转换成前束范式2.消去前束范式中的存在变量,略去其中的任意变量,生成SKOLEM标准形3.将SKOLEM标准形中