【本章小结】 本章讨论了谓词逻辑的等值和推理演算,是谓词逻辑的基本内容,主要内容可概括为: 1. 介绍了谓词逻辑公式等值的概念,引出了否定型等值式的不同形式及其证明方法; 2. 重点介绍了量词对不同联结词的分配率,即量词分配等值式,讨论了它们成立的条件和证明方法; 3. 从范式的概念出发,重点介绍了前束范式的定义以及Skolem标准形的构成,通过示例给出了化前束范式的过程,以及求前束范式和仅保留全称量词的前束范式的方法,并通过两个定理给出了这两种前束范式的普遍有效性和不可满足性与原公式的关系; 4. 介绍了基本的推理公式,给出了解释性的说明; 5. 详细介绍了有关量词的四条推理规则,并通过示例给出了使用推理规则进行推理演算的过程和方法; 6. 介绍了谓词逻辑的归结推理法,给出了归结推理法的正确性证明,并通过示例介绍了使用归结法证明推理公式的步骤和方法。 |