【章节小结】 　　本章叙述了命题逻辑的归结法基础。描述了将一个谓词逻辑公式化为Skolem标准形，得到相应的子句集的方法。介绍了归结法的一般过程，指出合一和置换是针对谓词逻辑归结的最重要的概念之一。并介绍了归结法的策略控制。 　　从Herbrand定理的有关内容可知，Herbrand定理是归结法的基础。虽然通过构造在H域上的语法树来判断一个谓词逻辑命题是否为永真，从而实现了将谓词逻辑转化成为命题逻辑判定问题，为Herbrand定理提供了实现的途径。最终还是归结原理使Herbrand定理成为现实可用的。