设a1,a2,…,an表示个体对象,A表示它们的属性、状态或关系,则表达式
A(a1,a2,…,an)在谓词逻辑中就表示一个(原子)命题。例如,(1)素数(2),就表示命题“2是个素数”。(2)好朋友(张三,李四),就表示命题“张三和李四是好朋友”。一般地,表达式
P(x1,x2,…,xn)在谓词逻辑中称为n元谓词。其中P是谓词符号，也称谓词，代表一个确定的特征或关系(名)。x1,x2,…,xn称为谓词的参量或者项，一般表示个体。个体变元的变化范围称为个体域（或论述域），包揽一切事物的集合称为全总个体域。为了表达个体之间的对应关系，我们引入通常数学中函数的概念和记法。例如我们用father(x)表示x的父亲，用sum(x,y)表示数x和y之和，一般地，我们用如下形式：
f(x1,x2,…,xn)表示个体变元x1,x2,…,xn所对应的个体y，并称之为n元个体函数，简称函数（或函词、函词命名式）。其中f是函数符号，有了函数的概念和记法，谓词的表达能力就更强了。
例如，我们用Doctor(father(Li))表示“小李的父亲是医生”，用E(sq(x),y))表示“x的平方等于y”。
以后我们约定用大写英文字母作为谓词符号,用小写字母f,g,h等表示函数符号,用小写字母x,y,z等作为个体变元符号,用小写字母a,b,c等作为个体常元符号。
其中M(x)表示“x是人”,N(x)表示“x有名字”,该式可读作“对于任意的x,如果x是人,则x有名字”。这里的个体域取为全总个体域。
同理,我们可以把命题“存在不是偶数的整数”表示为
其中G(x)表示“x是整数”,E(x)表示“x是偶数”。此式可读作“存在x,x是整数并且x不是偶数”。
不存在一个整数x,总比所有的整数y都大
任意的一个整数x,总有一个整数y比x大
例5.3某些人对某些食物过敏
定义1(1)个体常元和个体变元都是项。(2)设f是n元函数符号,若t1,t2,…,tn是项,则f(t1,t2,…,tn)是项。(3)只有有限次使用(1),(2)得到的符号串才是项。
定义2设P为n元谓词符号，t1,t2,…,tn为项，则P(t1,t2,…,tn)称为原子谓词公式，简称原子公式或者原子。从原子谓词公式出发，通过命题联结词和量词，可以组成复合谓词公式。下面我们给出谓词公式的严格定义，即谓词公式的生成规则。
定义3(1)原子公式是谓词公式。(2)若A,B是谓词公式，则A,A∧B,A∨B,A→B,AB,xA,xA也是谓词公式。(3)只有有限步应用(1)，(2)生成的公式才是谓词公式。由项的定义，当t1,t2,…,tn全为个体常元时，所得的原子谓词公式就是原子命题公式（命题符号）。所以，全体命题公式也都是谓词公式。谓词公式亦称为谓词逻辑中的合适（式）公式，记为Wff。
需要说明的是，仅个体变元被量化的谓词称为一阶谓词，如果不仅个体变元被量化，而且函数符号也被量化，这样的谓词称为二阶谓词。本书只涉及一阶谓词。把上面关于量化的概念也可以推广到谓词公式。于是，我们便可以说，如果一个公式中的所有个体变元都被量化，或者所有变元都是约束变元（或无自由变元），则这个公式就是一个命题。特别地，我们称xA(x)为全称命题，xA(x)为特称命题。对于这两种命题，当个体域为有限集时（设有n个元素），有下面的等价式：xA(x)A(a1)∧A(a2)∧…∧A(an)xA(x)A(a1)∨A(a2)∨…∨A(an)
这两个式子也可以推广到个体域为可数无限集。定义4设A为如下形式的谓词公式：
B1∧B2∧…∧Bn其中Bi(i=1,2,…,n)形如L1∨L2∨…∨Lm，Lj(j=1,2,…,m)为原子公式或其否定，则A称为合取范式。例如：(P(x)∨Q(y))∧(乛P(x)∨Q(y)∨R(x,y))∧(乛Q(y)∨乛R(x,y))就是一个合取范式。定义5设A为如下形式的命题公式：
B1∨B2∨…∨Bn其中Bi(i=1,2,…,n)形如L1∧L2∧…∧Lm，Lj(j=1,2,…,m)为原子公式或其否定，则A称为析取范式。例如：(P(x)∧乛Q(y)∧R(x,y))∨(乛P(x)∧Q(y))∨(乛P(x)∧R(x,y))就是一个析取范式。
定义6设P为谓词公式，D为其个体域，对于D中的任一解释：(1)若P恒为真，则称P在D上永真（或有效）或是D上的永真式。(2)若P恒为假，则称P在D上永假（或不可满足）或是D上的永假式。(3)若至少有一个解释,可使P为真，则称P在D上可满足或是D上的可满足式。定义7设P为谓词公式，对于任何个体域：(1)若P都永真，则称P为永真式。(2)若P都永假，则称P为永假式。(3)若P都可满足，则称P为可满足式。
例5.4设有前提：(1)凡是大学生都学过计算机；(2)小王是大学生。
试问：小王学过计算机吗？
解令S(x)：x是大学生;M(x)：x学过计算机;a：小王。则上面的两个命题可用谓词公式表示为(1)x(S(x)→M(x))(2)S(a)下面我们进行形式推理：(1)x(S(x)→M(x))［前提］(2)S(a)→M(a)[(1),US］(3)S(a)［前提］(4)M(a)［(2),(3),I3］得结果：M(a)，即“小王学过计算机”。
例5.5证明乛P(a,b)是xy(P(x,y)→W(x,y))和乛W(a,b)的逻辑结果。证(1)xy(P(x,y)→W(x,y))［前提］(2)y(P(a,y)→W(a,y))［(1),US］(3)P(a,b)→W(a,b)［(2),US］(4)乛W(a,b)［前提］(5)乛P(a,b)［(3),(4),I4］例5.6证x(P(x)→Q(x))∧(R(x)→乛Q(x))x(R(x)→乛P(x))。证
(1)x(P(x)→Q(x))［前提］(2)P(y)→Q(y)［(1),US］(3)乛Q(y)→乛P(y)［(2),E24］(4)x(R(x)→乛Q(x))［前提］(5)R(y)→乛Q(y)［(3),US］(6)R(y)→乛P(y)［(3),(5),I6］(7)x(R(x)→乛P(x))［(6),UG］
定义1原子谓词公式及其否定称为文字，若干个文字的一个析取式称为一个子句，由r个文字组成的子句叫r—文字子句，1—文字子句叫单元子句，不含任何文字的子句称为空子句，记为□或NIL。例如下面的析取式都是子句P∨Q∨乛RP(x,y)∨乛Q(x)
定义2对一个谓词公式G，通过以下步骤所得的子句集合S，称为G的子句集。
(1)消去蕴含词→和等值词←→。可使用逻辑等价式:①A→B乛A∨B②A←→B(乛A∨B)∧(乛B∨A)(2)缩小否定词的作用范围，直到其仅作用于原子公式。可使用逻辑等价式:①乛(乛A)A②乛(A∧B)乛A∨乛B③乛(A∨B)乛A∧乛B④乛xP(x)x乛P(x)⑤乛xP(x)x乛P(x)
由子句集的求法可以看出，一个子句集中的各子句间为合取关系，且每个个体变元都受全称量词约束（我们假定公式中无自由变元，或将自由变元看作常元）。所以，一个公式的子句集也就是该公式的Skolem标准型的另外一种表达形式。有了子句集，我们就可以通过一个谓词公式的子句集来判断公式的不可满足性。
定理1谓词公式G不可满足当且仅当其子句集S不可满足
定理1把证明一个公式G的不可满足性，转化为证明其子句集S的不可满足性。
定义3子句集S是不可满足的，当且仅当其全部子句的合取式是不可满足的。
归结演绎推理是基于一种称为归结原理(亦称消解原理principleofresolution)的推理规则的推理方法。归结原理是由鲁滨逊(J.A.Robinson)于1965年首先提出。它是谓词逻辑中一个相当有效的机械化推理方法。归结原理的出现，被认为是自动推理，特别是定理机器证明领域的重大突破。
定义4设L为一个文字，则称L与L为互补文字。
定义5设C1,C2是命题逻辑中的两个子句，C1中有文字L1，C2中有文字L2，且L1与L2互补，从C1,C2中分别删除L1,L2，再将剩余部分析取起来，记构成的新子句为C12，则称C12为C1,C2的归结式(或消解式)，C1,C2称为其归结式的亲本子句，L1,L2称为消解基。
例5.9设C1=乛P∨Q∨R,C2=乛Q∨S,于是C1,C2的归结式为
乛P∨R∨S
推论设C1,C2是子句集S的两个子句，C12是它们的归结式，则(1)若用C12代替C1,C2，得到新子句集S1，则由S1的不可满足可推出原子句集S的不可满足。即S1不可满足S不可满足(2)若把C12加入到S中，得到新子句集S2，则S2与原S的同不可满足。即S2不可满足S不可满足
例5.11证明子句集{P∨乛Q,乛P,Q}是不可满足的。证(1)P∨乛Q(2)乛P(3)Q(4)乛Q由(1),(2)(5)□由(3),(4)
例5.12用归结原理证明R是P,(P∧Q)→R,(S∨U)→Q,U的逻辑结果。证我们先把诸前提条件化为子句形式，再把结论的非也化为子句，由所有子句得到子句集S=｛P,乛P∨乛Q∨R,乛S∨Q,乛U∨Q,U,乛R｝，然后对该子句集施行归结，归结过程用下面的归结演绎树表示。由于最后推出了空子句，所以子句集S不可满足，即命题公式P∧(乛P∨乛Q∨R)∧(乛S∨Q)∧(乛U∨Q)∧U∧乛R
在一阶谓词逻辑中应用消解原理，不像命题逻辑中那样简单，因为谓词逻辑中的子句含有个体变元，这就使寻找含互否文字的子句对的操作变得复杂。例如：C1=P(x)∨Q(x)C2=乛P(a)∨R(y)直接比较，似乎两者中不含互否文字，但如果我们用a替换C1中的x，则得到C1′=P(a)∨Q(a)C2′=乛P(a)∨R(y)于是根据命题逻辑中的消解原理，得C1′和C2′的消解式C3′=Q(a)∨R(y)所以，要在谓词逻辑中应用消解原理，则一般需要对个体变元作适当的替换。定义6一个替换(Substitution)是形如｛t1/x1,t2/x2,…,tn/xn｝的有限集合，其中t1,t2,…,tn是项，称为替换的分子；x1,x2,…,xn是互不相同的个体变元，称为替换的分母；ti不同于xi，xi也不循环地出现在tj(i,j=1,2,…,n)中；ti/xi表示用ti替换xi。若t1,t2,…,tn都是不含变元的项（称为基项）时，该替换称为基替换；没有元素的替换称为空替换，记作ε，它表示不作替换。例如：例如：｛a/x,g(y)/y,f(g(b))/z｝就是一个替换，而{g(y)/x,f(x)/y}则不是一个替换,因为x与y出现了循环替换。
下面我们将项、原子公式、文字、子句等统称为表达式，没有变元的表达式称为基表达式，出现在表达式E中的表达式称为E的子表达式。
定义7设θ=｛t1/x1,…,tn/xn｝是一个替换，E是一个表达式，把对E施行替换θ，即把E中出现的个体变元xj(1≤j≤n)都用tj替换，记为Eθ，所得的结果称为E在θ下的例(instance)。定义8设θ=｛t1/x1,…,tn/xn｝,λ=｛u1/y1,…,um/ym｝是两个替换，则将集合｛t1λ/x1,…,tnλ/xn,u1/y1,…,um/ym｝中凡符合下列条件的元素删除：(1)tiλ/xi当tiλ=xi(2)ui/yi当yi∈｛x1,…,xn｝如此得到的集合仍然是一个替换，该替换称为θ与λ的复合或乘积，记为θ·λ。例5.13设θ=｛f(y)/x,z/y｝λ=｛a/x,b/y,y/z｝于是,｛t1λ/x1,t2λ/x2,u1/y1,u2/y2,u3/y3｝=｛f(b)/x,y/y,a/x,b/y,y/z｝从而θ·λ=｛f(b)/x,y/z｝可以证明，替换的乘积满足结合律，即(θ·λ)·u=θ·(λ·u)
定义9设S=｛F1,F2,…,Fn｝是一个原子谓词公式集，若存在一个替换θ，可使F1θ=F2θ=…=Fnθ，则称θ为S的一个合一(Unifier)，称S为可合一的。一个公式集的合一一般不唯一。定义10设σ是原子公式集S的一个合一，如果对S的任何一个合一θ，都存在一个替换λ，使得θ=σ·λ则称σ为S的最一般合一(MostGeneralUnifier)，简称MGU。例5.14设S=｛P(u,y,g(y)),P(x,f(u),z)｝，S有一个最一般合一σ=｛u/x,f(u)/y,g(f(u))/z｝对S的任一合一，例如：θ=｛a/x,f(a)/y,g(f(a))/z,a/u｝存在一个替换λ=｛a/u｝使得θ=σ·λ可以看出，如果能找到一个公式集的合一，特别是最一般合一，则可使互否的文字的形式结构完全一致起来，进而达到消解的目的。如何求一个公式集的最一般合一？有一个算法，可以求任何可合一公式集的最一般合一。为了介绍这个算法，我们先引入差异集的概念。
定义11设S是一个非空的具有相同谓词名的原子公式集，从S中各公式的左边第一个项开始，同时向右比较，直到发现第一个不都相同的项为止，用这些项的差异部分组成一个集合，这个集合就是原公式集S的一个差异集。
定义12设C1,C2是两个无相同变元的子句，L1,L2分别是C1,C2中的两个文字，如果L1和L2有最一般合一σ，则子句(C1σ-｛L1σ｝)∪(C2σ-｛L2σ｝)称作C1和C2的二元归结式(二元消解式)，C1和C2称作归结式的亲本子句，L1和L2称作消解文字。
例5.18设C1=P(x)∨Q(x),C2=P(a)∨R(y)，求C1,C2的归结式。
解取L1=P(x),L2=P(a),则L1与L2的最一般合一σ=｛a/x｝，于是,(C1σ-｛L1σ｝)∪(C2σ-｛L2σ｝)=(｛P(a),Q(a)｝-｛P(a)｝)∪(｛P(a),R(y)｝-｛P(a)｝)=｛Q(a),R(y)｝=Q(a)∨R(y)所以，Q(a)∨R(y)是C1和C2的二元归结式。
例5.19设C1=P(x,y)∨Q(a),C2=Q(x)∨R(y),求C1,C2的归结式。解由于C1,C2中都含有变元x,y，所以需先对其中一个进行改名,方可归结（归结过程是显然的，故从略）。还需说明的是，如果在参加归结的子句内部含有可合一的文字，则在进行归结之前，也应对这些文字进行合一，从而使子句达到最简。例如，设有两个子句：C1=P(x)∨P(f(a))∨Q(x)C2=P(y)∨R(b)可见,在C1中有可合一的文字P(x)与P(f(a))，那么，取替换θ={f(a)/x}(这个替换也就是P(x)和P(f(a))的最一般合一)，则得C1θ=P(f(a))∨Q(f(a))现在再用C1θ与C2进行归结，从而得到C1与C2的归结式Q(f(a))∨R(b)
定义13如果子句C中，两个或两个以上的文字有一个最一般合一σ，则Cσ称为C的因子，如果Cσ是单元子句，则Cσ称为C的单因子。
由以上例子可以看出，谓词逻辑中的消解原理也可以代替其他推理规则。上面我们通过推导空子句，证明了子句集的不可满足性，于是存在问题：对于任一不可满足的子句集，是否都能通过归结原理推出空子句呢？回答是肯定的。
定理5（归结原理的完备性定理）如果子句集S是不可满足的，那么必存在一个由S推出空子句□的消解序列。(该定理的证明要用到Herbrand定理，故从略。)
归结原理除了能用于对已知结果的证明外，还能用于对未知结果的求解，即能求出问题的答案来。请看下例。
例5.23已知:(1)如果x和y是同班同学，则x的老师也是y的老师。(2)王先生是小李的老师。(3)小李和小张是同班同学。问：小张的老师是谁？
解设谓词T(x,y)表示x是y的老师，C(x,y)表示x与y是同班同学，则已知可表示成如下的谓词公式：F1:xyz(C(x,y)∧T(z,x)→T(z,y))F2:T(Wang,Li)F3:C(Li,Zhang)为了得到问题的答案，我们先证明小张的老师是存在的，即证明公式：G:xT(x,Zhang)于是，求F1∧F2∧F3∧乛G的子句集如下:(1)乛C(x,y)∨乛T(z,x)∨T(z,y)(2)T(Wang,Li)(3)C(Li,Zhang)(4)乛T(u,Zhang)归结演绎，得(5)乛C(Li,y)∨T(Wang,y)由(1),(2),{Wang/z,Li/x}(6)乛C(Li,Zhang)由(4),(5),{Wang/u,Zhang/y}(7)□由(3),(6)
解先把上述前提中的三个命题符号化为谓词公式：F1:xyz(F(x,y)∧F(y,z)→G(x,z))F2:F(Lao,Da)F3:F(Da,Xiao)并求其子句集如下:(1)乛F(x,y)∨乛F(y,z)∨G(x,z)(2)F(Lao,Da)(3)F(Da,Xiao)设求证的公式为G:xyG(x,y)(即存在x和y，x是y的祖父)把其否定化为子句形式再析取一个辅助谓词GA(x,y)，得(4)乛G(u,v)∨GA(u,v)对(1)~(4)进行归结,得(5)乛F(Da,z)∨G(Lao,z)(1),(2),{Lao/x,Da/y}(6)G(Lao,Xiao)(3),(5),{Xiao/z}(7)GA(Lao,Xiao)(4),(6),{Lao/u,Xiao/v}所以，上述人员中，老李是小李的祖父。
前面我们介绍了归结原理及其应用，但前面的归结推理都是用人工实现的。而人们研究归结推理的目的主要是为了更好地实现机器推理，或者说自动推理。那么，现在就存在问题：归结原理如何在机器上实现？把归结原理在机器上实现，就意味着要把归结原理用算法表示，然后编制程序，在计算机上运行。下面我们给出一个实现归结原理的一般性算法：
步1将子句集S置入CLAUSES表；步2若空子句NIL在CLAUSES中，则归结成功，结束。步3若CLAUSES表中存在可归结的子句对，则归结之，并将归结式并入CLAUSES表，转步2；步4归结失败，退出。可以看出，这个算法并不复杂，但问题是在其步3中应该以什么样的次序从已给的子句集S出发寻找可归结的子句对而进行归结呢？
例5.27对下面的子句集S，我们用宽度优先策略与删除策略相结合的方法进行消解。S:(1)P(x)∨Q(x)∨乛R(x)(2)乛Q(a)(3)乛R(a)∨Q(a)(4)P(y)(5)乛P(z)∨R(z)可以看出，(4)类含了(1)，所以先将(1)删除。于是，剩下的四个子句归结得S1:(6)乛R(a)［(2),(3)］(7)乛P(a)∨Q(a)［(3),(5),{a/z}］(8)R(z)［(4),(5),{z/y}］
（6)出现后(3)可被删除，所以，第二轮归结在(2)、(4)、(5)、(6)、(7)、(8)间进行。其中(2)、(4)、(5)间的归结不必再重做，于是得S2:(9)乛P(a)［(2),(7)］(10)Q(a)［(4),(7),{a/y}］(11)乛P(a)［(5),(6),{a/z}］(12)□［(6),(8),{a/z}］
删除策略有如下特点：删除策略的思想是及早删除无用子句，以避免无效归结，缩小搜索规模；并尽量使归结式朝“小”（即元数少）方向发展。从而尽快导出空子句。删除策略是完备的。即对于不可满足的子句集，使用删除策略进行归结，最终必导出空子句□。定义一个归结策略是完备的，如果对于不可满足的子句集，使用该策略进行归结，最终必导出空子句□。
支持集策略：每次归结时，两个亲本子句中至少要有一个是目标公式否定的子句或其后裔。这里的目标公式否定的子句集即为支持集。
例5.28设有子句集S={乛I(x)∨R(x),I(a),乛R(y)∨乛L(y),L(a)}其中子句乛I(x)∨R(x)是目标公式否定的子句。
我们用支持集策略归结如下：
S:(1)乛I(x)∨R(x)(2)I(a)(3)乛R(y)∨乛L(y)(4)L(a)S1:(5)R(a)由(1),(2),{a/x}(6)乛I(x)∨乛L(x)由(1),(3),{x/y}S2:(7)乛L(a)由(5),(3),{a/y}(8)乛L(a)由(6),(2),{a/x}(9)乛I(a)由(6),(4),{a/x}(10)□由(7),(4)支持集策略有如下特点：这种策略的思想是尽量避免在可满足的子句集中做归结，因为从中导不出空子句。而求证公式的前提通常是一致的，所以，支持集策略要求归结时从目标公式否定的子句出发进行归结。所以，支持集策略实际是一种目标制导的反向推理。支持集策略是完备的。
线性归结策略：在归结过程中，除第一次归结可都用给定的子句集S中的子句外，其后的各次归结则至少要有一个亲本子句是上次归结的结果。线性归结的归结演绎树如图5―3所示，其中C0,B0必为S中的子句，C0称为线性归结的顶子句；C0,C1,C2,…,Cn-1称为线性归结的中央子句；B1,B2,…,Bn-1称为边子句，它们或为S中的子句，或为C1,C2,…,Cn-1中之一。
例5.29对例5.28中的子句集，我们用线性归结策略归结。(1)乛I(x)∨R(x)(2)I(a)(3)乛R(y)∨L(y)(4)L(a)(5)R(a)由(1)(2),{a/x}(6)乛L(a)由(5)(3),{a/y}(7)□由(6)(4)