【学习目标】
   通过本章的学习,应达到以下目标:
   ◇ 理解谓词逻辑公式等值的概念,掌握否定型等值式的不同形式及其证明方法;
   ◇ 了解量词对不同联结词的分配率,掌握量词分配等值式的证明方法;
   ◇ 理解范式的概念,掌握前束范式的定义以及Skolem标准形的构成,会求谓词逻辑公式的前束范式和仅保留全称量词的前束范式。了解它们的普遍有效性和不可满足性与原公式的关系;
   ◇ 熟悉谓词逻辑的基本推理公式,能够给出解释性的证明和其它推理公式正确性的判断;
   ◇ 理解谓词逻辑有关量词的四条推理规则,掌握使用推理规则进行推理演算的方法;
   ◇ 理解谓词逻辑的归结推理法的证明过程及其正确性,掌握用归结法证明推理公式的方法。

【学习指南】
   本章所讨论的谓词逻辑的等值和推理演算是谓词逻辑的基本内容,学习时应注意把握以下几点:
   ◇ 注意找出谓词逻辑公式与命题逻辑公式之间的内在联系。对于一些命题公式的等值式,可直接用谓词公式带入命题变项便可得谓词公式等值式。所以,从二者之间的关系与区别中加以理解和掌握,是学习谓词逻辑等值式的一个有效途径。
   ◇ 否定型等值式和量词分配等值式尽管数量较多,但都是成组出现,只要掌握每组的代表类型及证明思路,其它便可举一反三。
   ◇ 谓词公式的前束范式是本章的重要内容,学习时不但要了解前束范式的一般形式,还要清楚两类前束范式与原公式等值的充要条件。 前束范式对应普遍有效的公式,而全称量词的前束范式对应不可满足的公式,在使用归结法进行定理证明时将用到后一种前束范式。
   ◇ 从命题逻辑推理公式的局限性来理解谓词逻辑公式的必要性,基本推理公式要在理解的基础上记忆,并掌握其证明思路。
   ◇ 量词的消去和引入规则是谓词逻辑所特有的内容,也是推理演算的基础,应结合实例学习,熟练掌握使用推理规则进行推理演算的方法。
   ◇ 命题逻辑的归结法再引入量词和变元,构成谓词逻辑的归结法,所以如何消去量词是建立子句集的关键。归结法是重要的证明方法,证明过程及其正确性都在学习掌握的范围之内。

【重点和难点】
   本章的重点和难点如下:
   ◇ 量词分配等值式中,有些公式的正确性并非显而易见,这给记忆和证明带来了一定困难,应从证明的思路入手;
   ◇ 前束范式是本章学习的一个重要内容,前束范式一般形式和化前束范式的步骤和方法是学习掌握的重点和难点,同时要深入理解定理5.3.2和定理5.3.3的内容。清楚两种标准型的使用范围;
   ◇ 基本推理公式既多又长,难以理解记忆,也可视为学习的难点之一;
   ◇ 四条推理规则是推理演算的基础,也是学习的重点,但不难理解,结合示例学习是关键;
   ◇ 归结法便于计算机实现,在谓词逻辑中同样重要,归结法证明过程及其正确性证明是学习的重点。

【预习思考题】   
   ◇ 在谓词逻辑中等值是如何定义的?
   ◇ 谓词逻辑都有哪些与命题逻辑类似的等值公式,如何证明它们的正确性?
   ◇ 任一谓词公式是否可化为与之等值的范式?这种范式形式是否唯一?
   ◇ 如何使用范式来简化对任一公式的普遍有效性与不可满足性的判定?
   ◇ 在谓词逻辑中如何进行推理演算?如何处理谓词逻辑中出现的量词
   ◇ 归结法推理中是否也适用于谓词逻辑?如何使用归结法进行谓词推理公式的证明?