【课前思考】

　　复习数理逻辑，明白命题逻辑、一阶谓词逻辑的基本概念，熟练谓词演算，会求谓词公式的前束范式和Skolem标准形等。

　　【学习目标】

　　熟练掌握命题逻辑归结法，一阶谓词逻辑归结法，Herbrand定理，理解Herbrand定理给出了一阶逻辑的半可判定算法，明白归结法完备性的含义，掌握归结法的几种控制策略，能够运用归结法证明定理。

　　【学习方法】

　　掌握命题逻辑的归结法，一阶谓词逻辑的归结法，通过练习会利用归结法证明定理，理解归结法的完备性，掌握归结法的几种控制策略。

　　【本章要点】

　　掌握数理逻辑的谓词演算方法，理解逻辑是人工智能的基本工具。认识归结方法是实现定理机器证明的一种方法，归结过程简单明了，而且归结法对于谓词逻辑描述的定理集来说是完备的。熟悉定理的子句集描述以及归结过程，会用归结法证明定理。理解Herbrad定理给出了一阶逻辑的半可判定算法。归结法执行效率低，归结过程要注意使用控制策略。从程序实现角度看，Prolog语言的解释机理是以归结原理为基础的。

　　【知识点】