谓词归结子句形( Skolem 标准形)
为了能够像命题逻辑那样进行
归结，首先必须解决谓词逻辑中的
量词问题。
前束范式：如果A中的一切量词都位
于该公式的最左边（不含否定词），
且这些量词的辖域都延伸到公式的
末端。
谓词归结子句形( Skolem 标准形)
Skolem标准形
前束范式中消去所有的量词。
Skolem函数
如果某个存在量词是在其他任意量词
的辖域内，就存在某种依赖关系，可
以用一个函数描述这种依赖关系，叫
做Skolem函数。
谓词归结子句形( Skolem 标准形)
量词消去原则：
• 存在量词。将该量词约束的变量用任意
常量（ a，b等）或任意变量的函数
（f(x)，g(y)等）代替。
• 左边有任意量词的存在量词，消去时该
变量改写成为任意量词的函数；如没有，
改写成为常量。
• 任意量词。简单地省略掉该量词。
谓词归结子句形( Skolem 标准形)
例:将下式化为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))
谓词归结子句形( Skolem 标准形)
第四步，变量易名，存在量词左移，直至所
有的量词移到前面，得：
(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))
由此得到前述范式
谓词归结子句形( Skolem 标准形)
– 第五步，消去存在量词，略去任意量词
消去(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)
谓词归结子句形( Skolem 标准形)
• Skolem定理：
谓词逻辑的任意公式都可以化为
与之等价的前束范式，但其前束
范式不唯一。
注意：谓词公式G的Skolem标准形
同G并不等值。
谓词归结子句形
• 子句与子句集
– 文字：不含任何连接词的谓词公式。
– 子句：一些文字的析取（谓词的和）。
– 空子句：不含任何文字的子句。记作NIL或
□
– 子句集：所有子句的集合。
– 对于任何一个谓词公式G，都可以通过
Skolem标准形，建立起一个子句集与之对应。
谓词归结子句形
• 子句集S的求取：
– 将谓词公式G转换成前束范式；
– 生成Skolem标准形；
– 将各个子句提出，以“，”取代“Λ”，并
表示为集合形式 。
谓词归结子句形
• 定理 谓词公式G是不可满足的，当且
仅当其子句集 S是不可满足的。
– G与S不等价，但在不可满足的意义下是一
致的。
注意：G真不一定S真，而S真必有G真。
即： S => G
谓词归结子句形
• 定理的推广
–对于形如G = G
1
Λ G
2
Λ G
3
Λ …Λ G
n
的谓词公式
–G的子句集可以分解成几个部分单独处理。
– 有 S
G
= S
1
U S
2
U S
3
U …U S
n
则S
G
与 S
1
U S
2
U S
3
U …U S
n
在不可满
足的意义上是一致的。即S
G
不可满足
<=> S
1
U S
2
U S
3
U …U S
n
不可满足。
可以对一个复杂的谓词公式分而治之。
求取子句集例(1)
例：对所有的x,y,z来说，如果y是x的父亲，z又
是y的父亲，则z是x的祖父。又知每个人都有
父亲，试问对某个人来说谁是他的祖父？
求：用一阶逻辑表示这个问题，并建立子句集。
解：这里我们首先引入谓词：
• P(x, y) 表示y是x 的父亲
• Q(x, y) 表示y是x的祖父
• ANS(x) 表示问题的解答
求取子句集例(2)
对于第一个条件，“如果y是x的父亲， z又是y的父亲，则z是x
的祖父”，一阶逻辑表达式如下：
A1：(x)(y)(z)(P(x, y)∧P(y, z)→Q(x, z))
S A1：～P(x ,y)∨～P(y, z)∨Q(x, z)
对于第二个条件：“每个人都有父亲”，一阶逻辑表达式：
A2：(x)(y)P(x, y)
S A2：P(x,f(x))
对于结论：某个人是他的祖父
B：(x)(y)Q(x, y)
否定后得到子句： ～( (x)(y)Q(x, y))∨ANS(y)
S
～B：～Q(x, y)∨ANS(y)
则得到的相应的子句集为：{ S A1，S A2，S～B }
置换与合一
• 一阶谓词逻辑得归结比命题逻辑的
归结要复杂的多，其中一个原因就
是谓词逻辑公式中含有个体变量与
函数。
• 如P(x) ∨ Q(y)与~P(a) ∨ R(z)
• 所以要考虑置换与合一。即对变量
作适当的替换。
置换
• 置换：可以简单的理解为是在一个谓词公式中用
置换项去置换变量。
• 定义：
置换是形如{t1/x1, t2/x2, …, tn/xn}的有限集合。
其中，x1, x2, …, xn是互不相同的变量， t1, t2,
…, tn是不同于xi的项（常量、变量、函数）；ti/xi
表示用ti置换xi，并且要求ti与xi不能相同，而且xi
不能循环地出现在另一个ti中。
例如：
{a/x，c/y，f(b)/z}是一个置换。
{g(y)/x，f(x)/y}不是一个置换。
置换的合成
• 设＝{t1/x1, t2/x2, …, tn/xn}，
＝{u1/y1, u2/y2, …, un/yn}，是两个置换。
则与的合成也是一个置换，记作·。它是从集合
{t1·/x1, t2·/x2, …, tn·/xn, u1/y1, u2/y2, …,
un/yn }
中删去以下两种元素：
– 当ti=xi时，删去ti/xi (i = 1, 2, …, n);
– 当yi{x1,x2, …, xn}时，删去uj/yj (j = 1, 2, …, m)
最后剩下的元素所构成的集合。
合成即是对ti先做置换然后再做置换
置换的合成
• 例：
设：＝{f(y)/x, z/y}，＝{a/x, b/y, y/z}，求与的
合成。
解：先求出集合
{f(b/y)/x, (y/z)/y, a/x, b/y, y/z}＝{f(b)/x, y/y, a/x, b/y,
y/z}
其中，f(b)/x中的f(b)是置换作用于f(y)的结果；y/y
中的y是置换作用于z的结果。在该集合中，y/y满足
定义中的条件i，需要删除；a/x，b/y满足定义中的条
件ii，也需要删除。最后得
·＝{f(b)/x，y/z}
合一
• 合一可以简单地理解为“寻找相对变量的置换，
使两个谓词公式一致”。
• 定义：设有公式集F＝{F1，F2，…，Fn}，若存在
一个置换，可使F1＝F2＝…= Fn，则称是F的
一个合一。同时称F1，F2，... ，Fn是可合一的。
• 例：
设有公式集F＝{P(x, y, f(y)), P(a,g(x),z)}，则＝
{a/x, g(a)/y, f(g(a))/z}是它的一个合一。
注意：一般说来，一个公式集的合一不是唯一的。
最一般合一（mgu）
• 设σ是谓词公式集F的一个合一，如果对F的任意一
个合一都存在一个置换λ，使得θ=σ.λ，则称σ是一
个最一般合一。
• 最一般合一求取方法
– 令W={F1,F2}
– 令k=0,W0=W, σ0=ε
– 如果Wk已合一，停止， σk=mgu,否则找Dk
– 若Dk中存在元素vk和tk，其中，vk不出现在tk中，转下一
步，否则，不可合一。
– 令σk+1= σk.{tk/vk},Wk+1=Wk{tk/vk}=W σk+1
– K=k+1转第3步。
最一般合一（mgu）
例：W={P(a,x,f(g(y))),P(z,f(a),f(u))},其中，F1
＝ P(a,x,f(g(y)))，F2＝ P(z,f(a),f(u))
求F1和F2的mgu
解：由mgu算法
(1)W= {P(a,x,f(g(y))),P(z,f(a),f(u))}
(2)W0=W,σ0=ε
(3) W0 未合一，从左到右找差异集，有
D0={a,z}
(4)取V0=z,t0＝a
最一般合一（mgu）
(5)令σ1= σ0. {t0/v0}={a/z}
W1= W0 σ1={P(a,x,f(g(y))),P(a,f(a),f(u))}
(3)’ W1 未合一，找差异集，有D1={x,f(a)}
(4)’取v1=x,t1＝f(a)
(5)’令σ2=σ1. {t1/v1}= {a/z,f(a)/x}
W2= W1σ2={P(a,f(a),f(g(y))),P(a,f(a),f(u))}
(3)’’ W2 未 合 一 ， 找 差 异 集 ， 有
D2={g(y),u}
(4)’’取v2=u,t2＝g(y)
最一般合一（mgu）
(5)’’令 σ3=σ2.
{t2/v2}={a/z,f(a)/x,g(y)/u}
W3= W2 σ3={P(a,f(a),f(g(y))),P(a,f(a),f(g(y)))}
(3)’’’ W3 已合一
σ3= {a/z,f(a)/x,g(y)/u}
便是F1和F2的mgu。
算法的第(4)步，当不存在vk或不存在tk或出
现差异集为{x,f(x)},都会导致不可合一。
此时，算法返回失败。
最一般合一（mgu）
谓词逻辑的归结方法和命题逻辑基本相
同，但在进行归结之前，应采用最一般合一
方法对待归结的一对子句进行置换。然后再
判断是否可以进行归结。
归结原理
• 归结时的注意事项：
1. 谓词的一致性，P()与Q()， 不可以
2. 常量的一致性，P(a, …)与P(b,….)，
不可以。
3. 变量与函数，P(a, x, ….)与P(x,
f(x), …)，不可以；
4. 不能同时消去两个互补对，P∨Q与～P∨
～Q得空，不可以
1. 先进行内部简化再进行置换与合并。
归结原理
• 归结的过程
写出谓词关系公式 →
用反演法写出谓词表达式→
SKOLEM标准形 →
求子句集S →
对S中可归结的子句做归结 →
归结式仍放入S中，反复归结过程 →
得到空子句
命题得证。
例题“快乐学生”问题
例：假设任何通过计算机考试并获奖的人都是快乐
的，任何肯学习或幸运的人都可以通过所有的考
试，张不肯学习但他是幸运的，任何幸运的人都
能获奖。求证：张是快乐的。
• 解：先将问题用谓词表示如下：
• R1:任何通过计算机考试并获奖的人都是快乐的
(x)((Pass(x, computer)∧Win(x,
prize))→Happy(x))
• R2:“任何肯学习或幸运的人都可以通过所有考试
”
(x)(y)(Study(x)∨Lucky(x)→Pass(x, y))
例题“快乐学生”问题
• R3:“张不肯学习但他是幸运的”
～Study(zhang)∧Lucky(zhang)
• R4:“任何幸运的人都能获奖”
(x)(Luck(x)→Win(x,prize))
• 结论：“张是快乐的”的否定
～Happy(zhang)
• 由R1及逻辑转换公式:P∧W→H = ～（P∧W）∨ H ，得
(1)～Pass(x, computer)∨～Win(x, prize)∨Happy(x)
• 由R2： (2)～Study(y)∨Pass(y,z)
• (3)～Lucky(u)∨Pass(u,v)
• 由R3： (4)～Study(zhang)
• (5)Lucky(zhang)
• 由R4： (6)～Lucky(w)∨Win(w，prize)
• 由结论：(7)～Happy(zhang) （结论的否定）
• (8)～ Pass(w, computer)∨Happy(w)∨～ Luck(w) (1)(6)，
{w/x}
• (9)～Pass(zhang, computer)∨～Lucky(zhang) (8)(7)，
{zhang/w}
• (10) ～Pass(zhang, computer) (9)(5)
• (11) ～Lucky(zhang) (10)(3)，{zhang/u, computer/v}
• (12) ɓ � (11)(5)
第三章谓词逻辑与归结原理
• 概述
• 命题逻辑
• 谓词逻辑的归结法
• 归结过程的控制策略
• Herbrand定理
第三章谓词逻辑与归结原理
• 概述
• 命题逻辑
• 谓词逻辑的归结法
• 归结过程的控制策略
• Herbrand定理
归结过程的控制策略
• 要解决的问题：
– 归结方法的知识爆炸。
• 控制策略的目的
– 归结点尽量少
• 控制策略的原则
– 给出控制策略，以使仅对选择合适的子
句间方可做归结。避免多余的、不必要
的归结式出现。或者说，少做些归结仍
能导出空子句。
控制策略的方法(1)
删除策略
• 归类：设有两个子句C和D，若有置换使
得C D成立，则称子句C把子句D归类。
• 若对S使用归结推理过程中，当归结式Cj是
重言式和Cj被S中子句和子句集的归结式
Ci(i<j)所归类时，便将Cj删除。这样的推
理过程便称作使用了删除策略的归结过程。
控制策略的方法(1)
删除策略
• 如P(x)∨～P(x), P(x)∨Q(x)～P(x)
• P(x)归类P(y)∨Q(z) σ={y/x}
• 纯文字删除。如果某文字L在子句集中不存在可与
之互补的文字～L，则称该文字为纯文字。如
S={P∨Q∨R,～Q∨R,Q,～R}
• 尽管使用删除策略的归结，少做了归结但不
影响产生空子句，就是说删除策略的归结推
理是完备的。
控制策略的方法(2)
支撑集策略
• 支撑集：设有不可满足子句集S的子集T，
如果S-T是可满足的，则T是支撑集。
– 采用支撑集策略时，从开始到得
到空子句的整个归结过程中，只选取不
同时属于S-T的子句，在其间进行归结。
就是说，至少有一个子句来自于支撑集T
或由T导出的归结式。
控制策略的方法(2)
支撑集策略
– 例如：A1ΛA2ΛA3Λ～B中的～B可以作为支撑
集使用。要求每一次参加归结的亲本子句中，
至少应该有一个是由目标公式的否定（～B）所
得到的子句或者它们的后裔。
– 支撑集策略的归结是完备的。同样，所有可归
结的谓词公式都可以用采用支撑集策略达到加
快归结速度的目的。问题是如何寻找合适的支
撑集。一个最容易找到的支撑集是目标子句的
非，即S
～B。
S
T
可满足
支撑集示意图
控制策略的方法(2)
支撑集策略
• 例如：S
–(1)～I(X)∨R(X) 目标公式的否定得到的子句
–(2)I(a)
–(3)～R(Y)V～L(Y)
–(4)L(a)
• S1：
–(5) R(a) (1)与(2)归结
–(6) ～I(x)V～L(x) (1)与(3)归结
–(7)～L(a) (2)与(6)归结
–(8)NIL (4)与(7)归结
控制策略的方法(3)
语义归结策略
• 语义归结策略是将子句S按照一定的语义
分成两部分，约定每部分内的子句间不
允许作归结。同时还引入了文字次序，
约定归结时其中的一个子句的被归结文
字只能是该子句中“最大”的文字。
语义归结策略的归结是完备的。
控制策略的方法(4)
线性归结
• 线性归结策略首先从子句集中选取一个称
作顶子句的子句C0开始作归结。归结过程
中所得到的归结式Ci立即同另一子句Bi进
行归结得归结式Ci+1。而Bi属于S或是已出
现的归结式Cj(j<i)。即，如下图所示归结
得到的新子句立即参加归结。
线性归结是完备的。
C0 C1 C2 C3
C4
C5
空
线性归结策略示意图
控制策略的方法(5)
单元归结策略
• 单元归结策略要求在归结过程中，每次归结
都有一个子句是单元子句（只含一个文字的
子句）或单元因子。显而易见，此种方法可
以简单地削去另一个非单子句中的一个因子，
使其长度减少，构成简单化，归结效率较高。
初始子句集中没有单元子句时，单元归结策略无
效。所以说“反之不成立”，即此问题不能采用
单元归结策略。
控制策略的方法(6)
输入归结策略
• 与单元归结策略相似，输入归结策略要求
在归结过程中，每一次归结的两个子句中
必须有一个是S的原始子句。这样可以避
免归结出的不必要的新子句加入归结，造
成恶性循环。可以减少不必要的归结次数。
如同单元归结策略，不是所有的可归结谓词
公式的最后结论都是可以从原始子句集中的
得到的。
第三章谓词逻辑与归结原理
• 概述
• 命题逻辑
• 谓词逻辑的归结法
• 归结过程的控制策略
• Herbrand定理
第三章谓词逻辑与归结原理
• 概述
• 命题逻辑
• 谓词逻辑的归结法
• 归结过程的控制策略
• Herbrand定理
Herbrand定理
•问题：
一阶逻辑公式的永真性
（永假性）的判定是否
能在有限步内完成？
Herbrand定理
• 1936年图灵(Turing)和邱吉(Church)互
相独立地证明了：
“没有一般的方法使得在有限步内判定一阶
逻辑的公式是否是永真（或永假）。但是如果
公式本身是永真（或永假）的，那么就能在有
限步内判定它是永真（或永假）。对于非永真
（或永假）的公式就不一定能在有限步内得到
结论。判定的过程将可能是不停止的。”
Herbrand定理
• Herbrand的思想
–定义：
公式G永真：对于G的所有解释，G都为真。
–思想：
寻找一个已给的公式是真的解释。然而，如
果所给定的公式的确是永假的，就没有这样
的解释存在，并且算法在有限步内停止。
Herbrand定理
• H域
• H解释
• 语义树
• 结论：Herbrand定理
Herbrand定理
• H域
• H解释
• 语义树
• 结论：Herbrand定理
Herbrand定理（H域）
• 基本方法：
– 因为量词是任意的，所讨论的个体变量域D
是任意的，所以解释的个数是无限、不可数
的 。
– 简化讨论域。建立一个比较简单、特殊的域，
使得只要在这个论域上，该公式是不可满足
的。
– 此域称为H域。
D域
H域
H域与D域关系示意图
H域例题
• 设子句集S = { P(x), Q(y,f(z,b)),R(a)}，求H域
• 解：
H
0
＝ {a, b}为子句集中出现的常量
H
1
＝ {a, b, f(a,b), f(a,a), f(b,a), f(b,b)}
H
2
＝ { a, b, f(a,b), f(a,a), f(b,a), f(b,b)，
f(a,f(a,b)), f(a,f(a,a)), f(a, f(b,a)), f(a, f(b,b)),
f(b,f(a,b)), f(b,f(a,a)), f(b, f(b,a)), f(b,f(b,b)),
f(f(a,b),f(a,b)), f(f(a,b),f(a,a)), f(f(a,b), f(b,a)), f(f(a,b), f(b,b)),
f(f(a,a),f(a,b)), f(f(a,a),f(a,a)), f(f(a,a), f(b,a)), f(f(a,a), f(b,b)),
f(f(b,a),f(a,b)), f(f(b,a),f(a,a)), f(f(b,a), f(b,a)), f(f(b,a), f(b,b)),
f(f(b,b),f(a,b)), f(f(b,b),f(a,a)), f(f(b,b), f(b,a)), f(f(b,b), f(b,b))}
• ………
• H∞ = H1∪H2∪H3………
Herbrand定理（H域）
• 几个基本概念
–f（t
n
）：f为子句集S中的所有函数变量。t
1
,
t
2
, …t
n
为S的H域的元素。通过它们来讨论永
真性。
–原子集A：谓词套上H域的元素组成的集合。如
A = {所有形如 P(t
1
, t
2
, …t
n
)的元素}
即把H中的东西填到S的谓词里去。S中的谓词是
有限的，H是可数的，因此，A也是可数的。
原子集例题
上例题的原子集为：
• A = { P(a), Q(a, a), R(a), P(b), Q(b,
a),
Q(b, b), Q(a, b), R(b), P(
f(a,b)),
Q(f(a, b), f(a, b)), R(f(a, b),
P(f(a,a)), P(f(b,a)),
P(f(b,b)),……)
一旦原子集内真值确定好（规定好），则S在H
上的真值可确定。成为可数问题。
Herbrand定理
• H域
• H解释
• 语义树
• 结论：Herbrand定理
Herbrand定理
• H域
• H解释
• 语义树
• 结论：Herbrand定理
Herbrand定理（H解释）
• 解释I：谓词公式G在论域D上任何
一组真值的指定称为一个解释。
• H解释：子句集S在的H域上的解释
称为H解释。
问题：
对于所有的解释，全是假才可判定。
因为所有解释代表了所有的情况，如
可穷举，问题便可解决 。
Herbrand定理（H解释）
• 如下三个定理保证了归结法的正确性：
–定理1：
设I是S的论域D上的解释，存在对应于I的H解
释I*，使得若有S|
I
= T，必有 S|
I*
= T。
–定理2：
子句集S是不可满足的，当且仅当所有的S的H
解释下为假。
–定理3：
子句集S是不可满足的，当且仅当对每一个解
释I下，至少有S的某个子句的某个基例为假。
Herbrand定理（H解释）
• 基例
S中某子句中所有变元符号均以S的H域中的元素代入时，
所得的基子句C’称为C的一个基例。
• 若一个子句为假，则此解释为假。
• 一般来说，D是无穷不可列的，因此，子句集S也
是无穷不可列的。但S确定后H是无穷可列的。不
过在H上证明S的不可满足性仍然是不可能的。
• 解决问题的方法：语义树
Herbrand定理
• H域
• H解释
• 语义树
• 结论：Herbrand定理
Herbrand定理
• H域
• H解释
• 语义树
• 结论：Herbrand定理
Herbrand定理（语义树）
• 构成方法
–原子集中所有元素逐层添加的一棵二
叉树。将元素的是与非分别标记在两
侧的分枝上（可不完全画完） 。
• 特点
–一般情况H是无限可数集，S的语义树
是无限树。
N0
P(a)
N12
Q(a)
P(f(a))
N24
N31 N38
无限语义树
N11
~P(a)
~Q(a)
Q(a) ~Q(a)
~P(f(a))
N21
S＝{～P(x)∨Q(x)，P(f(y))，～
Q(f(y))}
Herbrand定理（语义树）
• 意义
– S H A 语义树
–可以理解语义树为H域的图形解释。
目的：把每个解释都摊开。语义树中包
含原子集的全部元素。因此，语义树是
完全的。每一个直到叶子节点的分支对
应S的一个解释。可以通过对语义树每一
个分支来计算S的真值。如果每个基例都
为假，则可认为是不可满足的。
Herbrand定理（语义树）
• 几个概念
–失败结点：
当（由上）延伸到点N时，I(N)已表明了S的某
子句的某基例为假。但N以前尚不能判断这个
事实。就称N为失败结点。
–封闭语义树：
如果S的完全语义树的每个分枝上都有一个失
败结点，就称它是一棵封闭语义树。
N0
P(a)
N1,2Q(a)
P(f(a)) N2,4
N3,1
N3,8
N1,1
N4,2N4,1
N2,1
N3,2
N2,2
N3,6
N4,9 N4,10 N4,13 N4,14
封闭语义树
Q(f(a))
S＝{～P(x)∨Q(x)，P(f(y))，～
Q(f(y))}
Herbrand定理
• H域
• H解释
• 语义树
• 结论：Herbrand定理
Herbrand定理
• H域
• H解释
• 语义树
• 结论：Herbrand定理
Herbrand定理（结论）
Herbrand定理：
1. 子句集S是不可满足的，当且仅当对应
于S的完全语义数是棵有限封闭树。
2. 子句集S是不可满足的，当且仅当存在
不可满足的S的有限基例集。
Herbrand定理（结论）
• 定理的意义
– Herbrand定理已将证明问题转化成了命题逻辑问题。
– 由此定理保证，可以放心的用机器来实现自动推理
了。（归结原理）
• 注意
– Herbrand定理给出了一阶逻辑的半可判定算法，即
仅当被证明定理是成立时，使用该算法可以在有限
步得证。而当被证定理并不成立时，使用该算法得
不出任何结论。
但是
Herbrand定理（结论）
• 仍存在的问题：
基例集序列元素的数目随子句集的元素数目成
指数地增加。
• 因此，Herbrand定理是30年代提出的，
始终没有显著的成绩。
直至1965年Robinson提出了归结原理。
归结原理与Herbrand定理
• 归结过程是语义树的倒塌过程
• 最后归结出空，就是剩一个根节
点，就说明语义树是有限封闭的，
证明结束。
习题：设已知：
(1)能阅读者是识字的；
(2)海豚不识字；
(3)有些海豚是很聪明的。
试证明：有些聪明者并不能阅读。
证 首先，定义如下谓词：
R(x)：x能阅读。
L(x)：x识字。
I(x)：x是聪明的。
D(x)：x是海豚。
然后把上述各语句翻译为谓词公式：
(1) x(R(x)→L(x))
(2) x(D(x)→ ﹁ L(x)) 已知条件
(3) x(D(x)∧I(x))
(4) x(I(x)∧﹁R(x)) 需证结论
求题设与结论否定的子句集，得
(1)﹁ R(x)∨L(x)
(2)﹁ D(y)∨ ﹁ L(y)
(3)D(a)
(4)I(a)
(5)﹁ I(z)∨R(z)
归结得
(6) R(a) (5)，(4)，{a/z}
(7) L(a) (6)，(1)，{a/x}
(8) ﹁ D(a) (7), (2), {a/y}
(9)□ (8), (3)
1.假设：所有不贫穷且聪明的人都快乐。那些看书的人是聪
明的。李明能看书且不贫穷。快乐的人过着激动人心的生活。
求证：李明过着激动人心的生活
给定谓词：某人x贫穷, Poor(x); 某人x聪明, Smart(x); 某人x,
快乐 happy(x); 某人x读书,Read(x); 某人x过着激动人心的生
活, Exciting(x)。
证明：
由前提：所有不贫穷且聪明的人都快乐
(x)( ～ Poor(x) ∧ Smart(x) → happy(x))
那些看书的人是聪明的
(x)(Read(x) → Smart(x))
李明能看书且不贫穷
Read(LM) ∧ ～ Poor(LM)
快乐的人过着激动人心的生活
(x) (happy(x) → Exciting(x))
由结论的否定
～ Exciting(LM)
子句集：
S = { Poor(x) ∨ ～Smart(x) ∨ happy(x), ～Read(y) ∨
Smart(y)， Read(LM), ～ Poor(LM) ， ～happy(z) ∨
Exciting(z) ， ～ Exciting(LM)}
