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这个定理成立。
