一、一階謂詞邏輯
1、謂詞、函數、量詞
設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等作為個體常元符號。
我們把“所有”、“一切”、“任一”、“全體”、“凡是”等詞統稱為全稱量詞, 記為 ∀x; 把“存在”、“有些”、“至少有一個”、 “有的”等詞統稱為存在量詞, 記為∃ x。 
其中M(x)表示“x是人”, N(x)表示“x有名字”, 該式可讀作“對於任意的x, 如果x是人, 則x有名字”。這里的個體域取為全總個體域。
如果把個體域取為人類集合, 則該命題就可以表示為
同理, 我們可以把命題“存在不是偶數的整數”表示為
其中G(x)表示“x是整數”, E(x)表示“x是偶數”。此式可讀作“存在x, x是整數並且x不是偶數”。
不同的個體變元, 可能有不同的個體域。為了方便和統一起見, 我們用謂詞表示命題時,一般總取全總個體域, 然后再采取使用限定謂詞的辦法來指出每個個體變元的個體域。 具體來講,有下面兩條：
(1) 對全稱量詞,把限定謂詞作為蘊含式之前件加入, 即 ∀x(P(x)→…)。
(2) 對存在量詞, 把限定量詞作為一個合取項加入, 即 ∃x(P(x)∧…)。
這里的P(x)就是限定謂詞。 我們再舉幾個例子。
例 5.1 不存在最大的整數, 我們可以把它翻譯為 
不存在一個整數x,總比所有的整數y都大
或
任意的一個整數x,總有一個整數y比x大
例 5.2 對於所有的自然數, 均有x+y>x 
例5.3 某些人對某些食物過敏
2、謂詞公式
定義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, A↔B, ∀xA, ∃xA也是謂詞公式。
(3)只有有限步應用(1)，(2)生成的公式才是謂詞公式。
由項的定義，當t1,t2,…,tn全為個體常元時，所得的原子謂詞公式就是原子命題公式（命題符號）。所以，全體命題公式也都是謂詞公式。謂詞公式亦稱為謂詞邏輯中的合適（式）公式，記為Wff。
緊接於量詞之后被量詞作用(即說明)的謂詞公式稱為該量詞的轄域。例如：
(1) ∀xP(x)。
(2) ∀x(H(x)→G(x, y))。
(3) ∃xA(x)∧B(x)。
其中(1)中的P(x)為∀x的轄域, (2)中的H(x)→G(x, y)為∀x的轄域, (3)中的A(x)為∃x的轄域, 但B(x)並非 ∃x的轄域。
量詞后的變元如 ∀x, ∃y中的x,y稱為量詞的指導變元(或作用變元), 而在一個量詞的轄域中與該量詞的指導變元相同的變元稱為約束變元, 其他變元(如果有的話)稱為自由變元, 例如(2)中的x為約束變元, 而y為自由變元, (3)中A(x)中的x為約束變元, 但 B(x)中的x為自由變元。例如(3),一個變元在一個公式中既可約束出現, 又可自由出現, 但為了避免混淆, 通常通過改名規則, 使得一個公式中一個變元僅以一種形式出現。
約束變元的改名規則如下：
(1) 對需改名的變元, 應同時更改該變元在量詞及其轄域中的所有出現。
(2) 新變元符號必須是量詞轄域內原先沒有的, 最好是公式中也未出現過的。例如公式 ∀xP(x)∧Q(x)可改為∀yP(y)∧Q(x), 但兩者的意義相同。
在謂詞前加上量詞, 稱作謂詞中相應的個體變元被量化, 例如∀xA(x)中的x被量化, ∃yB(y)中y被量化。如果一個謂詞中的所有個體變元都被量化, 則這個謂詞就變為一個命題。例如, 設P(x)表示“x是素數”,則 ∀xP(x), ∃xP(x)就都是命題。這樣我們就有兩種從謂詞(即命題函數)得到命題的方法：一種是給謂詞中的個體變元代入個體常元, 另一種就是把謂詞中的個體變元全部量化。
需要說明的是，僅個體變元被量化的謂詞稱為一階謂詞，如果不僅個體變元被量化，而且函數符號也被量化，這樣的謂詞稱為二階謂詞。本書只涉及一階謂詞。
把上面關於量化的概念也可以推廣到謂詞公式。於是，我們便可以說，如果一個公式中的所有個體變元都被量化，或者所有變元都是約束變元（或無自由變元），則這個公式就是一個命題。特別地，我們稱∀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為可滿足式。
3、謂詞邏輯中的形式演繹推理
由上節所述，我們看到，利用謂詞公式可以將自然語言中的陳述語句表示為一種形式化的符號表達式。那么，利用謂詞公式，我們同樣可以將形式邏輯中抽象出來的推理規則形式化為一些符號變換公式。表5.1和表5.2就是形式邏輯中常用的一些邏輯等價式和邏輯蘊含式，即推理規則的符號表示形式。 
例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)是 ∀x ∀y(P(x,y)→W(x,y))和乛W(a,b)的邏輯結果。證
(1) ∀x∀y(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、子句集
定義1 原子謂詞公式及其否定稱為文字，若干個文字的一個析取式稱為一個子句，由r個文字組成的子句叫r—文字子句，1—文字子句叫單元子句，不含任何文字的子句稱為空子句，記為□或NIL。
例如下面的析取式都是子句
P∨Q∨乛R
P(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)
(3)適當改名，使量詞間不含同名指導變元和約束變元。
(4)消去存在量詞。
消去存在量詞時，同時還要進行變元替換。變元替換分兩種情況：
①若該存在量詞在某些全稱量詞的轄域內，則用這些全稱量詞指導變元的一個函數代替該存在量詞轄域中的相應約束變元，這樣的函數稱為Skolem函數；
②若該存在量詞不在任何全稱量詞的轄域內，則用一個常量符號代替該存在量詞轄域中的相應約束變元，這樣的常量符號稱為Skolem常量。
(5)消去所有全稱量詞。
(6)化公式為合取范式。
可使用邏輯等價式:
①A∨(B∧C) ⇔ (A∨B)∧(A∨C)
②(A∧B)∨C ⇔ (A∨C)∧(B∨C)
(7)適當改名，使子句間無同名變元。
(8)消去合取詞∧，以子句為元素組成一個集合S。
例5.7 求下面謂詞公式的子句集
∀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)］}
由步(3)得 ∀x{ ∃yP(x,y)∨∃z［Q(x,z)∧乛R(x,z)］}
由步(4)得 ∀x{乛P(x,f(x))∨［Q(x,g(x))∧乛R(x,g(x))］}
由步(5)得 乛P(x,f(x))∨［Q(x,g(x))∧乛R(x,g(x))］
由步(6)得 ［乛P(x,f(x))∨Q(x,g(x))］∧［乛P(x,f(x))∨乛R(x,g(x))］
由步(7)得 ［乛P(x,f(x))∨Q(x,g(x))］∧［乛P(y,f(y))∨乛R(y,g(y))］
由步(8)得 {乛P(x,f(x))∨Q(x,g(x)),乛P(y,f(y))∨乛R(y,g(y))}
或
乛P(x,f(x))∨Q(x,g(x))
乛P(y,f(y))∨R(y,g(y))
為原謂詞公式的子句集。
需說明的是，在上述求子句集的過程中，當消去存在量詞后，把所有全稱量詞都依次移到整個式子的最左邊（或者先把所有量詞都依次移到整個式子的最左邊，再消去存在量詞），再將右部的式子化為合取范式，這時所得的式子稱為原公式的Skolem標准型。例如，上例中謂詞公式的Skolem標准型就是
∀x{［乛P(x,f(x))∨Q(x,g(x))］∧［乛P(y,f(y))∨乛R(y,g(y))］}
例5.8 設G=∀x∀y∀z∀u∀v∀w(P(x,y,z)∧乛Q(u,v,w))，那么，用a代替x，用f(y,z)代替u，用g(y,z,v)代替w，則得G的Skolem標准型
∀y∀z∀v(P(a,y,z)∧乛Q(f(y,z),v,g(y,z,v)))
進而得G的子句集為
{P(a,x,y),乛Q(f(u,v),w,g(u,v,w))}
由此例還可看出，一個公式的子句集也可以通過先求前束范式，再求Skolem標准型而得到。
需說明的是，引入Skolem函數，是由於存在量詞在全稱量詞的轄域之內，其約束變元的取值則完全依賴於全稱量詞的取值。Skolem函數就反映了這種依賴關系。但注意，Skolem標准型與原公式一般並不等價，例如有公式：
由子句集的求法可以看出，一個子句集中的各子句間為合取關系，且每個個體變元都受全稱量詞約束（我們假定公式中無自由變元，或將自由變元看作常元）。所以，一個公式的子句集也就是該公式的Skolem標准型的另外一種表達形式。有了子句集，我們就可以通過一個謂詞公式的子句集來判斷公式的不可滿足性。
定理1 謂詞公式G不可滿足當且僅當其子句集S不可滿足
定理1把證明一個公式G的不可滿足性，轉化為證明其子句集S的不可滿足性。
定義3 子句集S是不可滿足的，當且僅當其全部子句的合取式是不可滿足的。
2、命題邏輯中的歸結原理
歸結演繹推理是基於一種稱為歸結原理(亦稱消解原理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
定理2 歸結式是其親本子句的邏輯結果。
證明 設C1=L∨C1′,C2=乛L∨C2′,C1′,C2′都是文字的析取式，則C1,C2的歸結式為C1′∨C2′，因為
C1=C1′∨L=乛(C1′→L),C2=L∨C2′=(L→C2′)
所以
C1∧C2=(乛C1′→L)∧(L→C2′)⇒乛(C1′→C2′)=C1′∨C2′
證畢。
由定理2即得推理規則：
C1∧C2⇒ (C1-｛L1｝)∪(C2-｛L2｝) 
推論 設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
不可滿足，從而R是題設前提的邏輯結果。 
3、替換與合一
在一階謂詞邏輯中應用消解原理，不像命題邏輯中那樣簡單，因為謂詞邏輯中的子句含有個體變元，這就使尋找含互否文字的子句對的操作變得復雜。例如：
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的一個差異集。
例5.15 設S=｛P(x,y,z),P(x,f(a),h(b))｝，則不難看出，S有兩個差異集
D1=｛y,f(a)｝
D2=｛z,h(b)｝
設S為一非空有限具有相同謂詞名的原子謂詞公式集，下面給出求其最一般合一的算法。
合一算法(Unification algorithm)：
步1 置k=0, Sk=S，σk=ε;
步2 若Sk只含有一個謂詞公式，則算法停止，σk就是要 求的最一般合一;
步3 求Sk的差異集Dk;
步4 若Dk中存在元素xk和tk，其中xk是變元，tk是項且xk 不在tk中出現，則置Sk +1= Sk ｛tk/xk｝,σk+1=σk·｛tk/xk｝，k=k+1，然后轉步2;
步5 算法停止，S的最一般合一不存在。
例5.16 求公式集S=｛P(a,x,f(g(y))),P(z,h(z,u),f(u))｝的最一般合一。
解
k=0：
S0=S, σ0=ε,S0不是單元素集，求得D0=｛a,z｝，其中z是變元，且不在a中出現，所以有
σ1=σ0·｛a/z｝=ε·｛a/z｝=｛a/z｝
S1=S0｛a/z｝=｛P(a,x,f(g(y))),P(a,h(a,u),f(u))｝
k=1:
S1不是單元素集，求得D1=｛x,h(a,u)｝，
所以
σ2=σ1·｛h(a,u)/x｝=｛a/z｝·｛h(a,u)/x｝=｛a/u,h(a,u)/x｝
S2=S1｛h(a,u)/x｝=｛P(a,h(a,u),f(g(y))),P(a,h(a,u),f(u))｝
k=2:
S2不是單元素集，D2=｛g(y),u｝，
σ3=σ2·｛g(y)/u｝=｛a/z,h(a,g(y))/x,g(y)/u｝
S3=S2｛g(y)/u｝=｛P(a,h(a,g(y),f(g(y))),P(a,h(a,g(y)),f(g(y)))｝=｛P(a,h(a,g(y)),f(g(y)))｝
k=3:
S3已是單元素集，所以σ3就是S的最一般合一。
例5.17 判定S=｛P(x,x),P(y,f(y))｝是否可合一？
解
k=0:
S0=S,σ0=ε,
S0不是單元素集，D0=｛x,y｝
σ1=σ0·｛y/x｝=｛y/x｝
S1=S0｛y/x｝=｛P(y,y),P(y,f(y))｝
k=1:
S1不是單元素集，D1=｛y,f(y)｝，由於變元y在項f(y)中出現，所以算法停止，S不存在最一般合一。
從合一算法可以看出，一個公式集S的最一般合一可能是不唯一的，因為如果差異集Dk=｛ak,bk｝，且ak和bk都是個體變元，則下面兩種選擇都是合適的：
σk+1=σk·｛bk/ak｝或σk+1=σk·｛ak/bk｝
定理3 （合一定理）如果S是一個非空有限可合一的公式集，則合一算法總是在步2停止，且最后的σk即是S的最一般合一。本定理說明任一非空有限可合一的公式集，一定存在最一般合一，而且用合一算法總能找到最一般合一，這個最一般合一也就是當算法終止在步2時，最后的合一σk。
4、謂詞邏輯中的歸結原理
定義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.20 設C=P(x)∨P(f(y))∨乛Q(x),令σ=｛f(y)/x｝，於是Cσ=P(f(y))∨乛Q(f(y))是C的因子。
定義14 子句C1,C2的消解式，是下列二元消解式之一：
(1)C1和C2的二元消解式;
(2)C1和C2的因子的二元消解式;
(3)C1的因子和C2的二元消解式;
(4)C1的因子和C2的因子的二元消解式。
定理4 謂詞邏輯中的消解式是它的親本子句的邏輯結果。(證明類似於定理2，故從略。)
由此定理我們即得謂詞邏輯中的推理規則：
C1∧C2 ⇒ (C1σ-｛L1σ｝)∪(C2σ-｛L2σ｝)
其中C1,C2是兩個無相同變元的子句，L1,L2分別是C1,C2中的文字，σ為L1與L2的最一般合一。此規則稱為謂詞邏輯中的消解原理（或歸結原理）。
例5.21 求證G是A1和A2的邏輯結果。
A1: x(P(x)→(Q(x)∧R(x)))
A2: x(P(x)∧S(x))
G: x(S(x)∧R(x))
證 我們用反證法，即證明A1∧A2∧乛G不可滿足。首先求得子句集S：
(1)乛P(x)∨Q(x)
(2)乛P(y)∨R(y)
(3)P(a)
(4)S(a)
(5)乛S(z)∨乛R(z)(乛G)
然后應用消解原理，得
(6)R(a) ［(2),(3),σ1=｛a/y｝］
(7)乛R(a) ［(4),(5),σ2=｛a/z｝］
(8)□ ［(6),(7)］
所以S是不可滿足的，從而G是A1和A2的邏輯結果。
例5.22 設已知：
(1)能閱讀者是識字的；
(2)海豚不識字；
(3)有些海豚是很聰明的。
試證明：有些聰明者並不能閱讀。
證 首先，定義如下謂詞：
R(x)：x能閱讀。
L(x)：x識字。
I(x)：x是聰明的。
D(x)：x是海豚。
由以上例子可以看出，謂詞邏輯中的消解原理也可以代替其他推理規則。
上面我們通過推導空子句，證明了子句集的不可滿足性，於是存在問題：對於任一不可滿足的子句集，是否都能通過歸結原理推出空子句呢？回答是肯定的。
定理5 （歸結原理的完備性定理）如果子句集S是不可滿足的，那么必存在一個由S推出空子句□的消解序列。(該定理的證明要用到Herbrand定理，故從略。)
三、應用歸結原理求取問題答案
歸結原理除了能用於對已知結果的證明外，還能用於對未知結果的求解，即能求出問題的答案來。請看下例。
例5.23 已知:
(1)如果x和y是同班同學，則x的老師也是y的老師。
(2)王先生是小李的老師。
(3)小李和小張是同班同學。
問：小張的老師是誰？
解 設謂詞T(x,y)表示x是y的老師，C(x,y)表示x與y是同班同學，則已知可表示成如下的謂詞公式：
F1: x y z(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)
這說明，小張的老師確實是存在的。那么，為了找到這位老師，我們給原來的求證謂詞的子句再增加一個謂詞ANS(u)。於是，得到
(4)′ 乛T(u,Zhang)∨ANS(u)
現在，我們用(4)′代替(4)，重新進行歸結，則得
(5)′ 乛C(Li,y)∨T(Wang,y) 由(1)(2)
(6)′ 乛C(Li,Zhang)∨ANS(Wang) 由(4)′(5)′
(7)′ ANS(Wang) 由(3)(6)′
可以看出，歸結到這一步，求證的目標謂詞已被消去，即求證已成功，但還留下了謂詞ANS(Wang)。由於該謂詞中原先的變元與目標謂詞T(u,Zhang)中的一致，所以，其中的Wang也就是變元u的值。這樣，我們就求得了小張的老師也是王老師。
上例雖然是一個很簡單的問題，但它給了我們一個利用歸結原理求取問題答案的方法，那就是：先為待求解的問題找一個合適的求證目標謂詞；再給增配（以析取形式）一個輔助謂詞，且該輔助謂詞中的變元必須與對應目標謂詞中的變元完全一致；然后進行歸結，當某一步的歸結式剛好只剩下輔助謂詞時，輔助謂詞中原變元位置上的項（一般是常量）就是所求的問題答案。需說明的是，輔助謂詞（如此題中的ANS）是一個形式謂詞，其作用僅是提取問題的答案，因而也可取其他謂詞名。有些文獻中就用需求證的目標謂詞。如對上例，就取T(u,Zhang)為輔助謂詞。
例5.24 設有如下關系:
(1)如果x是y的父親，y又是z的父親，則x是z的祖父。
(2)老李是大李的父親。
(3)大李是小李的父親。
問：上述人員中誰和誰是祖孫關系？
解 先把上述前提中的三個命題符號化為謂詞公式：
F1: ∀x∀y∀z(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: ∃x∃yG(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、問題的提出
前面我們介紹了歸結原理及其應用，但前面的歸結推理都是用人工實現的。而人們研究歸結推理的目的主要是為了更好地實現機器推理，或者說自動推理。那么，現在就存在問題：歸結原理如何在機器上實現？把歸結原理在機器上實現，就意味着要把歸結原理用算法表示，然后編制程序，在計算機上運行。下面我們給出一個實現歸結原理的一般性算法：
步1 將子句集S置入CLAUSES表；
步2 若空子句NIL在CLAUSES中，則歸結成功，結束。
步3 若CLAUSES表中存在可歸結的子句對，則歸結之，並將歸結式並入CLAUSES表，轉步2；
步4 歸結失敗，退出。
可以看出，這個算法並不復雜，但問題是在其步3中應該以什么樣的次序從已給的子句集S出發尋找可歸結的子句對而進行歸結呢？
一種簡單而直接的想法就是逐個考察CLAUSES表中的子句，窮舉式地進行歸結。可采用這樣的具體作法：第一輪歸結先讓CLAUSES表(即原子句集S)中的子句兩兩見面進行歸結，將產生的歸結式集合記為S1，再將S1並入CLAUSES得CLAUSES＝S∪S1；下一輪歸結時，又讓新的CLAUSES即S∪S1與S1中的子句互相見面進行歸結，並把產生的歸結式集合記為S2，再將S2並入CLAUSES；再一輪歸結時，又讓S∪S1∪S2與S2中的子句進行歸結……如此進行，直到某一個Sk中出現空子句□為止。下面我們舉例。
例5.25 設有如下的子句集S，我們用上述的窮舉算法歸結如下：
S: (1)P∨Q
(2)乛P∨Q
(3)P∨乛Q
(4)乛P∨乛Q
S1:(5)Q ［(1),(2)］
(6)P ［(1),(3)］
(7)Q∨乛Q ［(1),(4)］
(8)P∨乛P ［(1),(4)］
(9)Q∨乛Q ［(2),(3)］
(10)P∨乛P ［(2),(3)］
(11)乛P ［(2),(4)］
(12)乛Q ［(3),(4)］
S2:(13)P∨Q ［(1),(7)］
(14)P∨Q ［(1),(8)］
(15)P∨Q ［(1),(9)］
(16)P∨Q ［(1),(10)］
(17)Q ［(1),(11)］
(18)P ［(1),(12)］
(19)Q ［(2),(6)］
(20)乛P∨Q ［(2),(7)］
(21)乛P∨Q ［(2),(8)］
(22)乛P∨Q ［(2),(9)］
(23)乛P∨Q ［(2),(10)］
(24)乛P ［(2),(12)］
(25)P ［(3),(5)］
(26)P∨乛Q ［(3),(7)］
(27)P∨乛Q ［(3),(8)］
(28)P∨乛Q ［(3),(9)］
(29)P∨乛Q ［(3),(10)］
(30)乛Q ［(3),(11)］
(31)乛P ［(4),(5)］
(32)乛Q ［(4),(6)］
(33)乛P∨乛Q ［(4),(7)］
(34)乛P∨乛Q ［(4),(8)］
(35)乛P∨乛Q ［(4),(9)］
(36)乛P∨乛Q ［(4),(10)］
(37)Q ［(5),(7)］
(38)Q ［(5),(9)］
(39)□ ［(5),(12)］
可以看出，這個歸結方法無任何技巧可言，只是一味地窮舉式歸結。因而對於如此簡單的問題，計算機推導了35步，即產生35個歸結式，才導出了空子句。那么，對於一個規模較大的實際問題，其時空開銷就可想而知了。事實上，這種方法一般會產生許多無用的子句。這樣，隨着歸結的進行，CLAUSES表將會越來越龐大，以至於機器不能容納。同時，歸結的時間消耗也是一個嚴重問題。
2、幾種常用的歸結策略
a.刪除策略
定義 設C1,C2是兩個子句，若存在替換θ，使得C1θ⊆C2，則稱子句C1類含C2。
例如：
P(x)類含P(a)∨Q(y) (只需取θ={a/x})
Q(y)類含P(x)∨Q(y) (θ=ε)
P(x)類含P(x),P(x)類含P(a),P類含P,P類含P∨R
P(a,x)∨P(y,b)類含P(a,b) (取θ={b/x,a/y})
刪除策略：
在歸結過程中可隨時刪除以下子句：
(1)含有純文字的子句；
(2)含有永真式的子句；
(3)被子句集中別的子句類含的子句。
所謂純文字，是指那些在子句集中無補的文字。例如下面的子句集
{P(x)∨Q(x,y)∨R(x),P(a)∨Q(u,v),Q(b,z),P(w)}中的文字R(x)就是一個純文字。
例5.26 我們在例3.25中使用刪除策略。可以看出，這時原歸結過程中產生的有些歸結式是永真式（如(7)、(8)、(9)、(10)），有些被前面已有的子句所類含（如(17)、(18)等，重復出現可認為是一種類含），因此，它們可被立即刪除。這樣就導致它們的后裔將不可能出現。於是，歸結步驟可簡化為
(1)P∨Q
(2)乛P∨Q
(3)P∨乛Q
(4)乛P∨乛Q
(5)Q ［(1),(2)］
(6)P ［(1),(3)］
(7)乛P ［(2),(4)］
(8)乛Q ［(3),(4)］
(9)□ ［(5),(8)］
其實，上述歸結還可以進一步簡化為
(5)Q ［(1),(2)］
(6)乛Q ［(3),(4)］
(7)□ ［(5),(6)］
這是因為，（5）式出來后，由於它類含了（1）、（2）式，所以可將（1）、（2）式刪除。同時當（6）式出現可將（3）、（4）式刪除。這樣也只能是（5）、（6）式歸結了。
例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}］
刪除策略有如下特點：
刪除策略的思想是及早刪除無用子句，以避免無效歸結，縮小搜索規模；並盡量使歸結式朝“小”（即元數少）方向發展。從而盡快導出空子句。
刪除策略是完備的。即對於不可滿足的子句集，使用刪除策略進行歸結，最終必導出空子句□。
定義 一個歸結策略是完備的，如果對於不可滿足的子句集，使用該策略進行歸結，最終必導出空子句□。
a.支持集策略
支持集策略：每次歸結時，兩個親本子句中至少要有一個是目標公式否定的子句或其后裔。這里的目標公式否定的子句集即為支持集。
例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)
支持集策略有如下特點：
這種策略的思想是盡量避免在可滿足的子句集中做歸結，因為從中導不出空子句。而求證公式的前提通常是一致的，所以，支持集策略要求歸結時從目標公式否定的子句出發進行歸結。所以，支持集策略實際是一種目標制導的反向推理。
支持集策略是完備的。
c.線性歸結策略
線性歸結策略：在歸結過程中，除第一次歸結可都用給定的子句集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)
其歸結反演樹如圖5―4所示。
線性歸結策略的特點是：不僅它本身是完備的，高效的，而且還與許多別的策略兼容。例如在線性歸結中可同時采用支持集策略或輸入策略。
4.輸入歸結策略
輸入歸結策略：每次參加歸結的兩個親本子句，必須至少有一個是初始子句集S中的子句。可以看出，例5.29中的歸結過程也可看作是運用了輸入策略。輸入歸結策略的特點是：
輸入歸結策略實際是一種自底向上的推理，它有相當高的效率。
輸入歸結是不完備的。例如子句集
S=｛P∨Q,乛P∨Q,P∨乛Q,P∨乛Q｝
是不可滿足的，用輸入歸結都不能導出空子句，因為最后導出□的子句必定都是單文字子句，它們不可能在S中。
輸入歸結往往同線性歸結配合使用，組成所謂線性輸入歸結策略。當然，進一步還可以與支持集策略結合。 