- 归结法的特点 　　归结法是与演绎法完全不同的，新的逻辑演算算法。它是一阶逻辑中，至今为止的最有效的半可判定的算法。也是最适合计算机进行推理的逻辑演算方法。 　　半可判定，即，一阶逻辑中任意恒真公式，使用归结原理，总可以在有限步内给以判定（证明其为永真式）。 - 归结法基本原理 　　归结法的基本原理是采用反证法或者称为反演推理方法，将待证明的表达式（定理）转换成为逻辑公式（谓词公式），然后再进行归结，归结能够顺利完成，则证明原公式（定理）是正确性的。 　　例如： 　　由命题逻辑描述的命题： A1、A2、A3 和 B，要求证明： 如果A1ΛA2ΛA3成立，则B成立， 　　即：A1ΛA2ΛA3 → B是重言式（永真式）。 　　归结法的思路是：A1ΛA2ΛA3 → B是重言式等价于A1ΛA2ΛA3Λ～B是矛盾式，也就是说永假式。 　　反证法：证明A1ΛA2ΛA3Λ～B 是矛盾式 　　（永假式） 　　归结的目的是建立基本规则证明该条定理（事实）成立。 - 归结法和其它推理方法的比较 　　语义网络、框架表示、产生式规则等知识表示方法的推理都是以逻辑推理方法为前提的。也就是说如果有了规则和已知条件，就能够依据一定的规则和公理顺藤摸瓜找到结果。 而本章所涉及的归结方法是计算机自动推理、自动推导证明用的。同样的内容可以"数学定理机器证明"中找到。 　　注意：本课程只讨论一阶谓词逻辑描述下的归结推理方法，不涉及高阶谓词逻辑问题 　　本章首先介绍了命题逻辑的归结，并以此为基础介绍了谓词逻辑的归结过程及相关的思想、概念和定义，最后给出了谓词逻辑归结的基础Herbrand定理的一般形式。