2.4 归结原理
本节在上节的基础上，进一步具体介绍谓词逻辑的归结方法。
谓词逻辑的归结法是以命题逻辑的归结法为基础，在Skolem 标准性的子句集上，通过置换和合一进行归结的。
下面先介绍一些本节中用到的必要概念：
一阶逻辑：谓词中不再含有谓词的逻辑关系式。
个体词：表示主语的词
谓词：刻画个体性质或个体之间关系的词
量词：表示数量的词
个体常量：a,b,c
个体变量：x,y,z
谓词符号：P,Q,R
量词符号：,
归结原理正确性的根本在于，如果在子句集中找到矛盾可以肯定命题是不可满足的。
2.4.1 合一和置换
置换：置换可以简单的理解为是在一个谓词公式中用置换项去置换变量。
定义：
置换是形如{t1/x1, t2/x2, …, t n/x n}的有限集合。
其中，x1, x2, …, x n是互不相同的变量，t1, t2, …, t n是不同于x i的项（常量、变量、函数）；t i/x i表示用t i置换x i，并且要求t i与x i不能相同，而且x i
不能循环地出现在另一个t i中。
例如
{a/x，c/y，f(b)/z}是一个置换。
{g(y)/x，f(x)/y}不是一个置换，原因是它在x和y之间出现了循环置换现象。
置换的目的是要将某些变量用另外的变量、常量或函数取代，使其不在公式中出现。
但在{g(y)/x，f(x)/y}中，它用g(y)置换x，用f(g(y))置换y，既没有消去x，也没有消去y。
若改为{g(a)/x，f(x)/y}就可以了。
通常，置换用希腊字母θ、σ、α、λ来表示的。
定义：置换的合成
设θ＝{t1/x1, t2/x2, …, t n/x n}，λ＝{u1/y1, u2/y2, …, u n/y n}，是两个置换。
则θ与λ的合成也是一个置换，记作θ·λ。
它是从集合{t1·λ/x1, t2·l/x2, …, t n·λ/x n, u1/y1, u2/y2, …, u n/y n}
即对ti先做λ置换然后再做θ置换，置换xi
中删去以下两种元素：
i. 当t iλ＝x i时，删去t iλ/x i(i = 1, 2, …, n);
ii. 当y i∈{x1,x2, …, x n}时，删去u j/y j(j = 1, 2, …, m)
最后剩下的元素所构成的集合。
例：
设θ＝{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)是置换l作用于f(y)的结果；y/y中的y 是置换λ作用于z的结果。
在该集合中，y/y满足定义中的条件i，需要删除；a/x，a/y满足定义中的条件ii，也需要删除。
最后得
θ·λ＝{f(b)/x，y/z}
合一：合一可以简单地理解为"寻找相对变量的置换，使两个谓词公式一致"。
定义：
设有公式集F＝{F1，F2，…，F n}，若存在一个置换θ，可使F1θ＝F2θ＝…= F nθ，则称θ是F的一个合一。
同时称F1，F2，... ，F n是可合一的。
例：
设有公式集F＝{P(x, y, f(y)), P(a,g(x),z)}，则λ＝{a/x, g(a)/y, f(g(a))/z}是它的一个合一。
注意：一般说来，一个公式集的合一不是唯一的。
定义：最一般合一
设σ是公式集F的一个合一，如果对F的任意一个合一θ
都存在一个置换λ，使得θ＝σ·λ，则称σ是一个最一般合一（Most General Unifier，简记为mgu）
一个公式集的最一般合一是唯一的。
若用最一般合一去置换
那些可合一的谓词公式，可使它们变成完全一致的谓词公式。
归结原理方法与命题逻辑基本相同。
但由于有变量与函数，所以要考虑合一和置换。
2.4.2 归结式
在谓词逻辑下求两个子句的归结式，和命题逻辑一样是消互补对，但需考虑变量的合一与置换。
设C1、C2是两个无公共变量的子句，L1、L2分别是C1、C2的文字，如果L1、～L2有mgu σ,则
(C1σ-{L1σ})∪(C2σ-{L2σ})
称作子句C1、C2的一个二元归结式，而L1、L2为被归结的文字。
归结式的注意事项：
·谓词的一致性，P()与Q()，不可以归结
·常量的一致性，P(a, …)与P(b,….)，不可以归结
·变量，P(a, ….)与P(x, …)，可以通过置换归结
变量与函数，P(a, x, ….)与P(x, f(x), …)，不可以归结；
但P(a, x, …)与P(x, f(y), …)，可以通过对两式分别做{f(y)/x}置换和{a/x}，再归结。
·不能同时消去两个互补对，形如P∨Q与～P∨～Q得空，是不正确的
·对子句集中的元素先进行内部简化（置换、合并）
例：
设C1＝P(y)∨P(f(x))∨Q(g(x))，C2＝～P(f(g(a)))∨Q(b)，求C1和C2的归结式。
解：
对C1，取最一般合一σ＝{f(x)/y}，得C1的因子
C1σ＝P(f(x))∨Q(g(x))
对C1的因子和C2进行归结，可得到C1和C2的归结式：Q(g(g(a)))∨Q(b)
2.4.3 归结过程
谓词逻辑的归结过程与命题逻辑的归结过程相比，其基本步骤相同，但每步的处理对象不同。
谓词逻辑需要把由谓词构成的公式集化为子句集，必要时在得到归结式前要进行置换和合一。
具体的谓词逻辑归结过程如下：
·写出谓词关系公式
·用反演法写出谓词表达式
·化为SKOLEM标准形
·求取子句集S
·对S中可归结的子句做归结
·归结式仍放入S中，反复归结过程
·得到空子句
·命题得证
例题2-4
"快乐学生"问题：
假设任何通过计算机考试并获奖的人都是快乐的，任何肯学习或幸运的人都可以通过所有的考试，张不肯学习但他是幸运的，任何幸运的人都能获奖。
求证：张是快乐的。
解：
先将问题用谓词表示如下：
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)
将上述谓词公式转化为子句集并进行归结如下：
首先将每一个表示逻辑条件的谓词子句转换为子句集可以接受的Skolem标准形。
由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) 结论的否定
根据以上7条子句，归结如下：
(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)归结
结论
1．归结法的实质：
·归结法是仅有一条推理规则的推理方法。
·归结的过程是一个语义树倒塌的过程。
2．归结法的问题
·对于传统归结法，子句中有等号或不等号时，完备性不成立。
即，传统的归结法不能处理相等的关系。
Herbrand定理式归结原理的理论基础；而正是由于Herbrand 定理的不实用性引出了可实用的归结法。