归结法是定理机器证明的重要方法，是仅有一条归结推理规则的机械推理法，它的优点是推理规则简便从而容易以程序实现，而且这种方法也可推广到谓词逻辑的推理。
一、归结证明过程
1.为证明A→B(可称作定理)是重言式, 依定理2.8.2等价于A∧?B是矛盾式。使用归结证明法，就是从A∧
B出发。
2.建立子句集S
3.对S作归结
4.直至归结出矛盾式□
B出发。