1、應用歸結之前，wff（合式公式）必須是一個范式或標準形式。范式有三種主要類型：

1）合取范式。如：

(P1∨P2....)∧(Q1∨Q2...)∧(Z1∨Z2...)

2）子句。

全子句形式的表達式通常如下：(表示A1,A2,...An全真是，B1，。。。Bn中至少有一個為真)

A1,A2,...An->B1,B2,.....Bn

3）HORN子句子集。

PROLOG使用HORN子句，只允許一個頭:

A1,A2,....An->B

用PROLOG可以寫成：

B:A1,A2,...An

2、歸結的基本目標是從兩個稱為根子句的子句推導出一個新的子句，即消解式。

1)A∨B

A∨~B

∴A

推導過程如下：

(A∨B)∧(A∨~B)≡A∨(B∧~B)≡A

3、歸結系統和演繹

給定wff

A1,A2,....An

∴C

1）歸結：

A1∧A2∧.....An->C≡~(A1∧A2∧......An)∨C≡~A1∨~A2∨...∨An∨C

2)反駁歸結：(證明了如果1）為重言式，則下式為矛盾式，即證明否定式為矛盾式)

~(A1∧A2∧.....An->C)≡~(~(A1∧A2∧......An)∨C)≡A1∧A2∧...∧An∧~C

4、反駁歸結樹：

如:

A->B

B->C

C->D

∴A->D

得出否定式：

~(~A∨D)≡A∧~D

樹如下，歸結得到的根是空的，表示為假，否定式為矛盾式

?

?

5、反駁歸結

設：

B=電池是好的 C=汽車能跑

E=有電F=火花塞能打火

G=有汽油R=發動機能工作

S=火花塞是好的 T=有好的輪胎

規則如下：

（1）（本條為結論規則，是一條定理，以下條為其它規則）B∧S∧G∧T->C

(2) B->E

(3) E∧S->F

(4)E∧G->R

(5)R∧T->C

首先，得出結論的否定式：

(1') ~(B∧S∧G∧T->C)=~(~B∨~S∨~G∨~T∨C)

接著，對其它規則進行變化：

(2') ~B∨E

(3') ~(E∧S)∨F=~E∨~S∨F

(4') ~(F∧G)∨R=~F∨~G∨R

(5') ~(R∧T)∨C=~R∨~T∨C

進行反駁歸結，樹如下：可以看到根為空，所以B∧S∧G∧T->C這個定理成立。