中科院讲义 人工智能 4.Herbrand定理_3

中科院讲义 人工智能

Herbrand定理张文生中国科学院自动化研究所

中科院讲义 人工智能

内容Skolem范式 Herbrand域语义树 Herbrand定理 Davis的工作

中科院讲义 人工智能

复习定义(定理)如果G是公式F1, F2,… Fn的逻辑结论,则公式 (F1∧F2∧…∧Fn)→G称为定理.

定理给定公式F1, F2,… Fn和G, G是公式F1, F2,… Fn的逻辑结论,当且仅当公式 F1∧F2∧…∧Fn∧~G不相容 (是永假式)。

中科院讲义 人工智能

Skolem范式 Herbrand域语义树 Herbrand定理 Davis的工作

中科院讲义 人工智能

化公式为Skolem范式的步骤公式化为前束范式母式化为合取范式在不影响公式的不相容性的前提下,使用Skolem函数，将前束中的存在量词消去

中科院讲义 人工智能

Skolem函数消去存在量词令公式H是一个前束范式，并且母式M是合取范式(Q1x1)…(Qnxn)(M)对前缀从左到右遇到的第一个存在量词Qr(1≤r≤n),存在两种情况:(1)如果Qr的左边(前边)没有全称量词,则M中的xr用常数a代替; (2)如果Qr的左边(前边)有全称量词xs1,…, xsk,且1≤s1<…<sk<r,则M中的xr用函数f(xs1,…, xsk)代替;

从前缀中删除(Qr xr);

中科院讲义 人工智能

例子(Skolem函数)( x)( y)( z)( u)( v)( w)P(x,y,z,u,v, w) ( y)( z)( u)( v)( w)P(a,y,z,u,v,w) ( y)( z)( v)( w)P(a,y,z,f(y,z),v,w) ( y)( z)( v)P(a,y,z,f(y,z),v,g(y,z,v))

中科院讲义 人工智能

注意要求a必须是新的常量符号，它未曾在公式其他地方使用过;要求f()不同于已出现在M中的任一函数，而对f的具体形式没有要求。

中科院讲义 人工智能

Skolem函数的意义化公式为Skolem范式与原来公式在不相容意义下保持等价(=).定理:令G是一个前束合取范式，G=(Q1x1)…(Qnxn)M[x1,…,xn],

Qr为G中从左向右遇到的第一个存在量词。令 G1=(Q1x1)…(Qr-1xr-1)(Qr+1xr+1)(Qnxn) M[x1,…,xr-1, f(x1,…,xr-1),xr+1,…,xn]其中：f(x1,…,xr-1)是xr的Skolem函数.

则有： G不相容 G1不相容

中科院讲义 人工智能

证明：(对存在量词xr使用归纳法)

设论域为D.由于G=(Q1x1)…(Qnxn)M[x1,…,xn], G1=(Q1x1)…(Qr-1xr-1)(Qr+1xr+1)…(Qnxn) M[x1,…,xr-1, f(x1,…,xr-1),xr+1,…,xn]一方面：如果G不相容假设G1相容:存在一个解释I,使得 G1=T.对任一组(x1,…,xr-1),都有f(x1,…,xr-1),使得 (Qr+1xr+1)…(Qnxn)M[x1,…,xr-1, f(x1,…,xr-1),xr+1,…,xn]为真. f(x1,…,xr-1)是D中一个元素.因此,对任一组(x1,…,xr-1), ( xr)(Qr+1xr+1)…(Qnxn)M[x1,…,xr,…,xn]=T ( x1)…( xr-1)( xr)(Qr+1xr+1)…(Qnxn)M[x1,…,xr,…,xn]=T即：G相容。

中科院讲义 人工智能

另一方面：如果G1不相容假设G相容:解释I: G=T.对任一组(x1,…,xr-1),存在一个元素xr∈D,使得 (Qr+1xr+1)…(Qnxn)M[x1,…,xr,…,xn]为真.扩充I为I’,使其包含对函数符号f(x1,…,xr-1)的指定: f(x1,…,xr-1)=xr,对任一组(x1,…,xr-1)对任一组(x1,…,xr-1), (Qr+1xr+1)…(Qnxn)M[x1,…, f(x1,…,xr-1),…,xn]为真. I’满足G1。

中科院讲义 人工智能

显然，如果公式前缀中有多个存在量词，则用归纳法证明。

中科院讲义 人工智能

注意Skolem范式和原式在不相容

意义下保持等价,而非等价(=)。如果G不相容,那么按照定理G=G1。如果G是相容的，一般情况下，G不等价于G1,即：G≠G1。

例子:G=( x)P(x) G1=P(a)在解释I下不相等:D={1,2} a=1, P(1)=F, P(2)=T.

G在I下为真, G1在I下为假.

中科院讲义 人工智能

将一个公式化为Skolem范式后,公式的到了简化，进一步我们还可以简化，那就是将公式化为子句集的形式.下面引入子句集的概念。

中科院讲义 人工智能

子句集Skolem化以后,将公式表示为子句集合. ( x)( y)((P(x)∨Q(y))∧ (Q(x)∨~S(f(y)))){P(x)∨Q(y), Q(x)∨~S(f(y))}定义(子句, clause):一个包含若干文字的析取式称为子句。例如：P∨~S∨ R P(x)∨ Q(y, z)∨~R(y, y)

说明：一个子句中没有文字则称空子句(, nil,永假);一个子句中有n个文字则称n文字子句。

定义(子句集合):子句内部的关系是析取;子句间的关系是合取;所有子句受全程量词约束;

中科院讲义 人工智能

化子句集的方法(9个步骤)例：( z) ( x)( y){[(P(x)∨Q(x))→R(y)]∨U(z)}1.消蕴涵符理论根据：a→b=~a∨b ( z) ( x)( y){[~(P(x)∨Q(x))∨ R(y)]∨U(z)} 2.移动否定符理论根据：~(a∨b)=~a∧~b~(a∧b)=~a∨~b~( x)P(x)= ( x)~P(x)~( x)P(x)= ( x)~P(x) ( z) ( x)( y){[(~P(x)∧~Q(x))∨ R(y)]∨U(z)}

中科院讲义 人工智能

3.变量标准化即：对于不同的约束，对应于不同的变量 ( x)A(x)∧ ( x)B(x)= ( x)A(x)∧ ( y)B(y) 4.量词左移 ( x)A(x)∧ ( y)B(y)= ( x)( y){A(x)∧ B(y)} 5.消存在量词 (skolem化) ( z)( x)( y){[(~P(x)∧~Q(x))∨ R(y)]∨ U(z)}=> ( x){[(~P(x)∧~Q(x))∨ R(f(x))]∨ U(a)}

中科院讲义 人工智能

6.化为合取范式即(a∨b)∧ (c∨d)∧ (e∨f)的形式( x){[(~P(x)∧~Q(x))∨ R(f(x))]∨ U(a)}=> ( x){(~P(x)∨ R(f(x))∨U(a))∧ (~Q(x)∨ R(f(x))∨U(a))}

7.隐去全程量词

{(~P(x)∨R(f(x))∨U(a))∧ (~Q(x)∨ R(f(x))∨U(a))

中科院讲义 人工智能

8.表示为子句集{~P(x)∨R(f(x))∨U(a),~Q(x)∨R(f(x))∨U(a)}

9.变量标准化(变量换名)

{~P(x1)∨R(f(x1))∨U(a),~Q(x2)∨R(f(x2))∨U(a)}

中科院讲义 人工智能

结论：定理(公式不相容基本定理)设S是公式G的子句集, G不相容 S不相容

说明：S不相容:对任一个解释, S中至少有一个子句为假; S相容:存在一个解释,使S中所有子句为真;

中科院讲义 人工智能

推论：如果G=G1∧…∧Gn, Si是Gi的子句集, i=1,…,n.令S’=S1∪…∪Sn. G不相容 S’不相容