人工智能导论课件：第四章 谓词逻辑与归结原理

1、1,第四章 谓词逻辑与归结原理,2,命题逻辑 经典逻辑 逻辑 谓词逻辑 缺省逻辑 非经典逻辑 非单调逻辑 模糊逻辑等等 归结原理是一种主要基于谓词逻辑知识表示的推理方法。,3,谓词逻辑,命题逻辑有一定的局限性. 例如: 不能表达这样的事实”当移动木块B时,说它就是on_B_C所断言的木块C上的木块. 命题演算中,原子是没有内部结构的串. 而谓词演算提供了这种能力,例如, 不再让一个命题符号P表示整个句子”星期二下雨了”,而是创建一个谓词Weather来描述日期和天气的关系.,4,一阶谓词逻辑的语法,一阶谓词逻辑的符号组成 常量, 变量,函数符号,谓词符号, 联结词: , , , , 量词: ,

2、 分隔符号: 逗号,括号 项的定义: 1) 常量,变量是项 2) 若f是n元函数,t1,tn是项,则 f(t1,tn)是项,5,合式公式,合式公式(wff)的定义: 1) 若p是n元谓词, t1,tn是项, 则 p(t1,tn)是合式公式. (称为原子) 2) 若F ,G是合式公式,则F, FG, FG, FG, FG 都是合式公式. 3) 若X是一个变量,F是合式公式,则xF, xF 也是合式公式. 举例: xp(X)y(p(Y)q(Y,X,f(a)）,6,谓词逻辑,是一种形式语言，具有严密的理论体系 是一种常用的知识表示方法, 例： City（北京） City（上海） Age（张三，23）

3、 (X)(Y)(Z)(father(X, Y)father(Y, Z)gf(X, Z),7,归结原理,归结原理是一种定理证明方法，1965年由J.A.Robinson提出，从理论上解决了定理证明问题。当时被认为是人工智能领域的重大突破。 该方法简单，易实现，因此一经提出，就得到了人们的广泛关注，对机器定理证明的研究起到了很大的推动作用。 但归结原理也不是无所不能, 例如:“连续函数之和仍连续”是微积分中的简单事实,可用归结原理证明时,推了十万步(归结出几十万个子句)仍无结果.,8,子句,归结原理是在谓词逻辑公式的子句集合上进行归结的。 定义:子句是如下形式的合式公式(wff): (L1 Ls

4、) 每个Li是文字(原子或原子的非),9,子句集,不包含任何文字的子句称为空子句。 子句集：所有子句的合取，且每个合取子句不包括相同的变量。 I(z)R(z), I(A), R(x) L(x), D(y) 例如： I(z)R(z), I(A), (R(x)L(x), D(y) 不是子句集。,10,一般的wff与子句之间的关系？,任一合式公式都可以转化成子句集,11,化子句集的方法,举例说明 例：x( p(X)y(p(Y) q(Y,X,f(a) x(p(X)y (p(Y)q(Y,X,f(a) （1） 去掉蕴涵 理论根据：ab a b x(p(X)y(q(Y,X,f(a)p(Y) x(p(X)y(

5、q(Y,X,f(a)p(Y),12,(2) 移动否定符，将内移到原子公式前: 理论根据：(a b) a b (a b) a b (x)P(x) (x)P(x) (x)P(x) (x)P(x) x (p(X)y(q(Y,X,f(a) p(Y) x( p(X) y(q(Y,X,f(a) p(Y) (3) 变量标准化，将各约束变量换名, 以避免混淆，即：不同的 约束，对应于不同的变量 (x)A(x) (x)B(x) (x)A(x) (y)B(y) x(p(X)y(q(Y,X,f(a) p(Y) u (p(U) v(q(V,U,f(a) p(V),化子句集的方法（续）,13,化子句集的方法（续）,去掉

6、 (skolem变换) 原式为：x(p(X)y(q(Y,X,f(a) p(Y) u (p(U) v(q(V,U,f(a) p(V) 去掉后： (p(c)y(q(Y,c,f(a) p(Y) u ( p(U) (q(h(U),U,f(a) p(h(U) (5) 将全称量词提到最前面: 所用公式：(ByA(X)y(BA(X) y u (p(c)(q(Y,c,f(a) p(Y) (p(U) (q(h(U),U,f(a) p(h(U),skolem变换: 将谓词公式中所有存在量词消去,得到该谓词公式的skolem标准型. 在消去存在量词时, 有两种情况: a. 存在量词不在任何全称量词的辖域内, 例如:

7、 x (X) 变为(c), (注: c必须是一个新的常量,称为skolem常数,不能在原来的中) b. 存在量词在某些全称量词的辖域内, 例如: xy height(X,Y)(公式中X依赖于Y) 变为 x height (X, h(X)） 这里h(X)称为Skolem函数.,略去全称量词为: (p(c)(q(Y,c,f(a) p(Y) ( p(U) (q(h(U),U,f(a) p(h(U) (6) 将上式化为合取范式 (p(c)(q(Y,c,f(a) p(Y) ( p(U)(q(h(U),U,f(a)( p(U) p(h(U) （7）表示为子句的形式 p(c)，q(Y,c,f(a) p(Y)

8、，p(U) q(h(U),U,f(a)， p(U) p(h(U) 注意：转化，保证不可满足性,16,说明：,转化不意味着等价性,但可保证其保持“不可满足性”. 一个合式公式或者一个子句集“不可满足”, 是指在任何解释下都有矛盾. 原式有矛盾，变换后的式子也有矛盾。,17,第11次课 11月28日,18,上次课程回顾,一阶谓词逻辑 子句，子句集 任一合式公式都可以转化成子句集, 不等价，但满足“不可满足性”,19,练习,求下面合式公式的子句集 x(yp(X,Y)y(q(X,Y)r(X,Y) 注: 按下面的步骤: 去掉蕴涵 将内移到原子公式前: 将各约束变量换名, 以避免混淆 去掉 (skolem

9、变换) 将全称量词提到最前面: 化为合取范式 化为子句集的形式,20,作业解答,求下面合式公式的子句集 x(yp(X,Y)y(q(X,Y)r(X,Y) 解答： 1)(去蕴涵)x(yp(X,Y)y(q(X,Y)r(X,Y) 2)(移否定)x(yp(X,Y) y(q(X,Y)r(X,Y) x(yp(X,Y) y (q(X,Y)r(X,Y) 3）(换名)x(yp(X,Y) z (q(X,Z)r(X,Z),21,定理,定理： 一个合式公式不可满足,当且仅当它所转化的子句集不可满足.,22,归结原理,在定理证明系统中，已知一公式集F1，F2，Fn，问公式W是否成立？ 方法一：证明F1F2FnW是永真式。

10、如果直接应用推理规则进行推导，不容易建立机器证明系统。 方法二：间接法（反证法），证明F1F2FnW为永假，可以通过证明F所对应的子句集S=S0W是不可满足的。,23,命题： P|=F PF是不可满足的。 证明: 若P F是不可满足的，则 P|= F 若P|=F 则 P F是不可 满足的。（反证法）,24,x(yp(X,Y) z (q(X,Z)r(X,Z) 5) (Skolem标准化) x(p(X,f(Y) (q(X,f(Z)r(X,f(Z) 6）（去全称量词）(p(X,f(X)(q(X,G(X)r(X,H(X) 7) (p(X,f(X)(q(X,G(Z) (p(X,f(X)r(X,H(X),

11、25,归结原理,基本思想 将待证明的逻辑公式的结论（F），通过等值公式转换成附加前提，再证明该逻辑公式是不可满足的。 F （已证） P|=F PF是不可满足的,26,使用归结原理证明的思路,目标（G）的否定连同已知条件（）一起，化为子句集 （ G化为子句集）， 并给出一种变换的方法，使得S S1 S2 . Sn同时保证当Sn不可满足时，有S不可满足。,27,使用归结原理证明的思路,目标（G）的否定连同已知条件（）一起，化为子句集 （ G化为子句集）， 并给出一种变换的方法，使得S S1 S2 . Sn同时保证当Sn不可满足时，有S不可满足。,空子句出现,给出一种转化方法，若原公式是永假的， 则

12、转化的子句集也是不可满足的。,把目标的否定化为子句集,28,归结方法（命题逻辑）,设子句集中的任意两个子句：C1=LC1C2=(L)C2 (消去互补）构成一个新的子句C=C1C2 则称这一过程为归结。C是C1和C2的归结式. 例1：设C1=PQR, C2=Q S， 例2：设 C1=P， C2=P 例3：设C1=PQ，C2=QR，C3=P， 两次归结：首先C1和C2 ，得C12=PR，再对C12，C3归结，得 C123=R。,29,归结方法（命题逻辑）,定理：归结式是两原子句的逻辑推论。或者说，任一使C1 ，C2为真的解释I下，必有归结式C12也为真。 证明:假设I是使C1 ，C2为真的任一解释

13、。,归结的例子,设集合： P, (PQ) R, (ST) Q, T 求证：R 子句集： (1) P (2) PQR (3) SQ (4) TQ (5) T (6) R（目标求反）,化子句集： (PQ) R = (PQ)R = PQR (ST) Q = (ST)Q = (ST)Q = (SQ) (TQ) = SQ, TQ,31,子句集： (1) P (2) PQR (3) SQ (4) TQ (5) T (6) R（目标求反）,归结： (7) PQ (2, 6) (8) Q (1, 7) (9) T (4, 8) (10) nil (5, 9),归结的例子,32,谓词逻辑的归结原理,谓词逻辑中，

14、由于子句中包含有变元，所以不能直接消去互补文字（L和L），故需要考虑变量的约束问题，即在应用归结法时，往往要对公式作变量置换和合一等处理，才能得到互补的基本式，然后进行归结。 问题：如何找归结对 例：P(x)Q(y), P(f(y)R(y),33,置换,定义: 置换是形如t1/x1,tn/xn的有限集,其中xi是互不相同的变量,ti是不等于xi的项,且xi与ti互不循环出现. 如果ti都是不含变量的项(基项),称该置换为基置换. 若= ,则称为空置换(表示不做置换),记为. 例如:1) a/x,g(y)/y,f(g(b)/z是一个置换? (是, 但不是基置换). 2) y/x, x/y是置换么

15、? (不是, 因为x,y循环出现).,34,置换（续）,定义 令 =t1/x1,tn/xn,E为表达式,E经所得的实例E也是一个表达式,它是把在E中出现的xi同时置换为ti而得到. (项,文字,文字的合取,析取均称为表达式) 若E是不含变量的表达式,则称其为E的一个基实例. 例如:令E为p(x,y,f(a) =b/x,f(x)/y,则 E= ? E=p(b,f(x),f(a) 此例显示了同时置换的含义. 可以看到E是在E上的作用,也就是将E中的(i=1, ,n)同时换成相应的ti所得到的公式.,35,置换乘法,定义 令 =s1/y1,sm/ym, =t1/x1,tn/xn,则与的复合是一个置换

16、,定义为: =s1 /y1,sm /ym, t1/x1,tn/xn -(si /yi| si= yiti/xi |xiy1 , ym) 注意: 乘法的直观含义是先做,在做.上述乘法的意思是从 s1 /y1,sm /ym, t1/x1,tn/xn中删除: (1) 若s1= yi,则删除si /yi项. (2) 若xiy1 , ym,则删除ti/xi . 所得到的新的置换.,例1. =f(y)/x,z/y, =a/x, b/y, y/z 则=f(y)/x,z/y, a/x, b/y, y/z -(si /yi| s1= yit1/x1 |x1y1 , ym) = f(b)/x,y/y, a/x,

17、b/y, y/z -(si /yi| s1= yit1/x1 |x1y1 , ym) =f(b)/x, y/z =a/x, b/y, y/z, f(y)/x,z/y -(si /yi| s1= yit1/x1 |x1y1 , ym) =a/x, b/y, z/z, f(y)/x, z/y -(si /yi| s1= yit1/x1 |x1y1 , ym) =a/x,b/y 可以看到: ,即乘法是不可交换的.,例2. 公式E=p(x,f(y),z),置换 =f(x,y)/z, z/w =a/x,b/y,w/z 求 (1) (E) (2) E() (3) E() 解:(1) E= p(x,f(y)

18、,z)f(x,y)/z, z/w = p(x,f(y),f(x,y) (E)=p(x,f(y),f(x,y)a/x,b/y,w/z =p(a,f(b),f(a,b) (2) =f(x,y)/z, z/w, a/x,b/y,w/z -(si /yi| s1= yit1/x1 |x1y1 , ym) =f(a,b)/z, w/w, a/x,b/y,w/z -(si /yi| s1= yit1/x1 |x1y1 , ym) =f(a,b)/z,a/x,b/y,E()= p(x,f(y),z)f(a,b)/z, a/x,b/y = p(a,f(b),f(a,b) (3) =a/x,b/y,w/z, f

19、(x,y)/z, z/w -(si /yi| s1= yit1/x1 |x1y1 , ym) =a/x, b/y, z/w E()= p(x,f(y),z)a/x, b/y, z/w =p(a,f(b),z) 明显的: E()E() 虽然置换乘法不满足交换律,但是满足下列性质: = (E)=E(), 其中E为任意公式. ()=() (即满足结合律),39,合一(unifier),最广合一(mgu),定义: 令S是一个简单表达式的非空有限集 S=E1,En, S=E1 ,En 若S是单元素集,即E1= =En,则称为S的一个合一(unifier), S称为是可合一的. 如果对S的任意一个合一,存

20、在一个置换,使的=,则称是S的一个最广合一(most general unifier),记为mgu. 可以看到,若S有合一,则称S是可合一的;否则,称S是不可合一的; 注意到合一不唯一.,前面介绍了合一和最广合一的概念. 为什么要求出最广合一? 求最广合一mgu的目的是: 使子句集中子句的文字形式结构完全一致,从而达到取消互补文字的目的。 例1. S=p(x), p(a) =a/x是一个mgu. 例2. S=p(x), p(f(y), =f(y)/x是一个mgu. 对于=f(a)/x,a/y也是一个合一 (因为S是一个单元素集). 可求得=a/y使得=.,41,例3. S=p(x), p(y)

21、, 1=x/y和 2=y/x均为S的mgu. 1= 2x/y= 21, 2= 1y/x=22, 由此例可知: 最广合一mgu不唯一. 若一个S有两个mgu,则经两个mgu变换后,所得到的结果只有变量不同. (S1 =p(x), S2 =p(y).,合一,42,第12次课 11月4日,43,上次课程回顾,归结: 1）两个子句：C1=LC1, C2=(L)C2 归结式为 C=C1C2 2）P(x)Q(y), P(f(y)R(y) 置换： t1/x1,tn/xn的有限集 置换乘法 合一，mgu,44,合一算法,在介绍合一算法前,首先了解差异集的概念. 差异集: 设S是一个非空的具有相同谓词名的原子公

22、式集,从S中各公式的左边第一项开始,同时向右比较,直到发现第一个不都相同的项为止,用这些项的差异部分组成一个集合,这个集合就是原子公式子句集的一个差异集. 例如: S=p(x,y,z),p(x,f(a),h(b), 则S的差异集D1=y,f(a),合一算法: 输入:简单表达式的非空有限集S. 输出: 判断S是否可合一; 若S可合一,则输出一个mgu. 若S不可合一,则报告S不可合一. 分析思路： 算法如下: 令k=0,Sk=S, k= 若Sk是单元素集,则算法停止,mgu=k 否则,求Skk的差异集Dk 若Dk中存在元素xk和tk,其中xk是变量, tk是项,且xk不出现在tk中,则置 k=k

23、+1,Sk+1= Sktk/xk,K+1=k tk/xk,转步骤2. 否则,算法停止,报告S不可合一. 说明:若S可合一,算法总是在步骤2停止. (也可画出框图),46,k=0,Sk=S0=S,k= Sk是单元素集么? Y S可合一,mgu=k 寻找Sk的差异集Dk Dk中元素xk和tk,其中xk是变量, Y 算法停止, tk是项,判断xk是否出现在tk中, S不可合一. N 置 k=k+1, Sk+1= Sktk/xk, K+1 =k tk/xk,Occur检查,47,举例,例1.求公式集S=p(a,x,f(g(y),p(z,h(z,u),f(u)的mgu. 解: 1) k=0, Sk=S0

24、=S, k=0=, 明显的, S0=S不是单元素集. 2) 求得其差异集D0=a,z,其中z为变量,a为项,且z不 在a中出现. 令k=k+1,有 1= 0 a/z= a/z= a/z S1=S0a/z=p(a,x,f(g(y),p(z,h(z,u),f(u)a/z =p(a,x,f(g(y), p(a,h(a,u),f(u) S1不是单元素集.,48,求得其差异集D1=x,h(a,u),其中x为变量,h(a,u)为项,且x不在h(a,u)中出现. 令k=k+1,有 2= 1h(a,u)/x=a/zh(a,u)/x = a/z,h(a,u)/x S2=S1 h(a,u)/x=p(a,x,f(g

25、(y), p(a,h(a,u),f(u)h(a,u)/x =p(a,h(a,u),f(g(y),p(a,h(a,u),f(u) S2不是单元素集. 求得其差异集D2=g(y),u,其中u为变量, g(y)为项,且u不在g(y)中出现.,举例（续）,49,令k=k+1,有 3=2g(y)/u=a/z,h(a,u)/xg(y)/u =a/z,h(a,g(y)/x S3=S2g(y)/u =p(a,h(a,u),f(g(y),p(a,h(a,u),f(u)g(y)/u =p(a,h(a,g(y),f(g(y),p(a,h(a,g(y),f(g(y) 明显的, S3是单元素集. 3) Mgu = 3=

26、a/z,h(a,g(y)/x,举例（续）,50,练习,1.令公式集S=p(a,x,h(g(z), p(z,h(y),h(y)使用合一算法,求S的mgu. 2. 判断S=p(x,x),p(y,f(y)是否可合一.,51,谓词逻辑的归结方法,对于子句C1L1和C2 L2，如果L1与L2可合一，且是其合一，则(C1C2)是其归结式。 例： P(x)Q(y), P(f(z)R(z) 判断（P(x)， P(f(z)）是否有合一 ? 若可以合一，则归结式为 (Q(y)R(z) ,52,谓词逻辑的归结举例,设集合： （1）(x)(R(x)L(x) （2）(x)(D(x)L(x) （3）(x)(D(x)I(x

27、) 求证： (x)(I(x)R(x) 化子句集： (x)(R(x)L(x) = (x)(R(x)L(x) 去全称量词：R(x)L(x),（2） (x)(D(x)L(x) = (x)(D(x)L(x) 去全称量词：D(x)L(x) （3）(x)(D(x)I(x) Skolem标准化 D(A)I(A) 即得：D(A) I(A),53,目标求反： (x)(I(x)R(x) 得 (x)(I(x)R(x) 得 (x)(I(x)R(x) 得 I(x)R(x),换名后的子句集： R(x1)L(x1) D(x2)L(x2) D(A) I(A) I(x5)R(x5),归结举例（续）,54,上例的归结树,子句集：

28、 R(x1)L(x1) D(x2)L(x2) D(A) I(A) I(x5)R(x5),I(A),I(x5)R(x5),R(A), A/x5,R(x1)L(x1),L(A), A/x1,D(x2)L(x2),D(A), A/x2,D(A),nil,55,基于归结的问答系统,例： 已知：(x)AT(John, x) AT(Fido, x) AT(John, School) 求证：(x)AT(Fido, x) 子句集： AT(John, x1) AT(Fido, x1) AT(John, School) AT(Fido, x2),指John在什么地方，Fido在什么地方,Fido在一个地方，找这个

29、地方,56,AT(Fido, x2),AT(John, x1) AT(Fido, x1),子句集：AT(John, x1) AT(Fido, x1) AT(John, School) AT(Fido, x2),x2/x1,AT(John, School),School/x2,AT(Fido, School),57,一个家族关系的例子,设有某家庭成员的集合 a, b, c1, c2, c3, d1, d2, d3, d4 并且知道它们之间的关系为: 1) b 是 c1, c2, c3的母亲. 2) c3 是 d4 的母亲. 3) c1是 d1, d2, d3的父亲. 4) a是 b的丈夫. 问题

30、：a的孙辈是谁?,58,问题分析,家庭的关系图. (1) mother(b, c1) (2) mother(b, c2) (3) mother(b, c3) (4) mother(c3, d4) (5) father(c1, d1) (6) father(c1, d2) (7) father(c1, d3) (8) husband(a, b),家庭中有三个二元关系: 母子关系,父子关系,夫妻关系.可表示为: mother (X,Y) : X是Y 的母亲. father (X,Y): X是Y 的父亲. huaband (X,Y): X是Y 的丈夫.句的形式,59,问题分析（续）,问题是: a的孙

31、辈是谁? 定义如下, 对任给 X, Y, Z a) 若X 是Y的母亲且Y是Z的母亲, 则X是Z的外祖母. b) 若X 是Y的母亲且Y是Z的父亲, 则X是Z的祖母. c) 若X 是Y的丈夫且Y是Z的(外)祖母, X是Z的(外)祖父. 形式的表示如下: (9) mother(X,Z) mother(Z,Y) grandmother(X,Y) (10) mother(X,Z) father(Z,Y) grandmother(X,Y) (11) husband(X,Z)grandmother(Z,Y) grandfather(X,Y),60,问题表示,已知：(1) mother(b, c1) (2)

32、mother(b, c2) (3) mother(b, c3) (4) mother(c3, d4) (5) father(c1, d1) (6) father(c1, d2) (7) father(c1, d3) (8) husband(a, b) (9) mother(X,Z) mother(Z,Y) grandmother(X,Y) (10) mother(X,Z) father(Z,Y) grandmother(X,Y) (11) husband(X,Z) grandmother(Z,Y) grandfather(X,Y) 求：(X) grandfather(a,X),(9) moth

33、er(X1,Z1) mother(Z1,Y1) grandmother(X1,Y1) (10) mother(X2,Z2) father(Z2,Y2) grandmother(X2,Y2) (11) husband(X3,Z3) grandmother(Z3,Y3) grandfather(X3,Y3),目标求反 grandfather(a,X4),61,归结, grandfather(a,X4), husband(X3,Z3) grandmother(Z3,Y3) grandfather(X3,Y3), husband(a,Z3) grandmother(Z3,Y3),a/X3，Y3/X4,

34、62,第13次课 11月11日,63,上次课程回顾,合一算法 谓词逻辑的归结,64,Herbrand定理,Herbrand定理是归结原理的理论基础。,Jacques Herbrand ： (1908.2.121931.7.27) 法国数学家, 生于法国巴黎, 死于一次登山事故. Herbrand定理的提出者。 Herbrand定理是归结原理的理论基础，归结原理的正确性是通过Herbrand定理证明的。,65,预备知识,谓词逻辑合式公式的真值： 1）原子公式的值要么为T, 要么为F. 2）若A,B为合式公式, 那么A, AB, AB, AB, AB的值由真值表决定. 3) 如果在解释I下,A对X

35、的所有赋值都是 T，那么XA的值是T，否则为F。 4）如果在解释中存在一个赋值使A的值是T， 那么XA的值是T，否则为F。 简单的说: 对谓词公式中的各种变量指定特定的常量去代替, 就构成了谓词的解释.,66,举例,例： 给定解释I如下: 论域 D=2,3; 函数f(x)为f(2)=3,f(3)=2； 谓词p(x)为p(2)=0，p(3)=1； q(x,y)为q(i,j)=1, i, j=2,3 r(x,y)为r(2,2)=r(3,3)=1, r(2,3)=r(3,2)=0 求（1）在解释I下，x(p(f(x)q(x,f(x)的 真值。 （2）在解释I下，xy r(x,y)的真值。 (3) 在

36、解释I下， xy r(x,y)的真值。,67,模型,对于公式F，公式集S和解释I： （1）若在I下，F为真，则I是F的一个模型。 （2）若在I下，S中各公式均为真，则I是S的 一个模型。 （3）如果S有模型，则称S是可满足的。 （4）如果S无模型，则称S是不可满足的。 （5）如果S的任一模型都是F的模型,则称F是 S的逻辑推论,记为 S|= F. 公式F永真：对于F的所有解释，F都为真。 公式F永假：对于F的所有解释，F都为假。,S= F1, F2, F3 ,68,Herbrand定理思想,为了证明一个谓词公式A永真, 需要证明其反命题A永假. 所谓“永假”就是不存在模型,即在所有可能的解释中

37、, A均取假值. 由于量词是任意的，所讨论的个体变量域D是任意的，所以解释的个数是无限的, 不可数的，要找到所有的解释是不可能的。 Herbrand定理的基本思想是简化讨论域，建立一个比较简单的，特殊的论域（Herbrand域），使得只要在此论域上，原谓词公式是不可满足的，即保证不可满足的性质不变。,69,Herbrand域和D域的关系如图：,D 域,H 域,70,Herbrand域,定义1：设S是一个子句集，U0是S中子句所含的全体常量集。若S中子句皆不含常量，则任择一常量a, 并令 U0 =a, 对i1, 令 Ui = Ui-1fn(t1,tn)| n1,fn是S中出现的所有函数符号的集合函数; t1,tnUi-1 Us= i0 Ui 则称Ui为S的i阶常量集, Us称为S的Herbrand论域. Us的元素称为基项.,71,举例,例1：令S=p(X),q(Y)r(Z)，求：H-域 解 在题目中设有常量a U0=a U1=U0=a Us=U0U1U3= a 例2: 令S=p(a),q(X)r(f