王捍贫，男，博士，北京大学信息科学技术学院教授，博士生导师，软件研究所副所长，人工智能学会离散数学专委会副主任。长年从事离散数学、形式化方法及算法设计与分析的教学和研究工作。主持完成多项国家研究课题，撰写和翻译出版了多部离散数学和计算理论教材，曾获得北京市教学成果奖一等奖。系国家级精品课“离散数学”课程主讲教师。主讲“数理逻辑”(离散数学3)。

一、授课学时安排 
    
       数理逻辑：2学时/次，共计24次，48学时；（下学期讲授）  

二、教学计划大纲  

第二十六章 命题演算
要点：命题联结词，命题演算形式推演系统N 与P 中的推演，可靠性与完全性定理
要求：
􀁺 熟练掌握命题及联结词的概念，五个常用的联结词（与、或、非、蕴涵、等价）
及其真假性定义；
􀁺 掌握自然语言命题的符号化。
􀁺 熟练掌握命题形式，指派的概念，命题真值表及其构造作方法。
􀁺 了解哑元及命题的真假值与哑元的无关性。
􀁺 熟练掌握真值函数，联结词完全性的概念。联结词与、或、非、蕴涵、等价构
成的集合及其子集合的完全性。与、或、非、蕴涵、等价之间的互相表示（如
果能够的话）
􀁺 掌握2 元真值函数构成的的集合及其子集合的完全性。
􀁺 熟练掌握有效推理形式的定义及其证明方法
􀁺 熟练掌握N 的构成，包括N 的公式的形成规则、公理集和形式推理规则。N 中
形式证明序列和内定理的定义。N 中内定理的证明技巧，如一些辅助定理（增
加前提律，传递率）和常见的内定理。
􀁺 掌握N 中公式的括号的省略规则。
􀁺 了解N 的证明序列的斜形和树形书写方式。
􀁺 熟练掌握P 的构成，包括P 的公式的形成规则、公理集和形式推理规则。P 中
形式证明序列和内定理的定义。P 中内定理的证明技巧。P 中常见内定理的证明。
􀁺 掌握P 中公式的简写规则。
􀁺 了解N 的证明序列的斜形书写方式。
􀁺 熟练掌握P 中有前提的证明序列的定义。演绎定理的内容和证明和使用。
􀁺 熟练掌握N 和P 的构成方式的差别。N 和P 的等价性定理的内容及其证明。
􀁺 掌握N 和P 的等价性定理的使用。
􀁺 熟练掌握指派，公式的真值及其求法，公式的分类（永真式，可满足式，永假
式）及其关系。逻辑蕴涵和逻辑等价（等值）概念。等值演算，包括基本等值
式和两个替换定理
􀁺 了解限制性公式及其性质。
􀁺 熟练掌握合取范式和析取范式的定义，范式存在性定理，范式的两种求法（真
值表法和等值算法）。
􀁺 掌握范式的不唯一性
􀁺 了解联结词完全集的另一证明方式。
􀁺 熟练掌握可靠性、和谐性和完备性的内容及其证明。 

第二十七章 一阶谓词演算
要点：量词，边元的约束与自由，一阶谓词演算形式推演系统NL 与KL 中的推演，可靠
性与完全性定理
要求：
􀁺 熟练掌握个体变元、个体常元、谓词、函数、量词（全称和存在）等概念。
􀁺 掌握自然语言命题的符号化。
􀁺 熟练掌握逻辑符号非逻辑符号，项，一阶公式。
􀁺 掌握常见数学对象的一阶语言公式的描述，包括代数结构等
􀁺 了解公式的括号的省略规则。
􀁺 熟练掌握辖域，自由（约束）出现，自由（约束）变元，项对变元在公式中自
由（可代入）。
􀁺 了解闭项，闭式，全称闭式。
􀁺 熟练掌握NL 的构成，包括NL 的公式的形成规则、公理集和形式推理规则。NL 中
形式证明序列和内定理的定义。NL 中内定理的证明技巧，如一些辅助定理（代
入实例，增加前提律，传递率，）和常见的内定理（如换名规则）。
􀁺 了解NL 的证明序列的斜形和树形书写方式。
􀁺 熟练掌握前束范式的定义，范式存在性定理，范式的求法（包括所用的几个内
定理）
􀁺 了解根据范式对一阶公式进行分类。
􀁺 熟练掌握KL 的构成，包括KL 的公式的形成规则、公理集和形式推理规则。KL
中形式证明序列和内定理的定义。KL 中内定理的证明技巧。KL 中常见内定理的
证明。
􀁺 掌握KL 中公式的简写规则。
􀁺 了解KL 的证明序列的斜形书写方式。
􀁺 熟练掌握P 中有前提的证明序列的定义。演绎定理的内容和证明和使用。
􀁺 熟练掌握NL 和KL 的构成方式的差别。N L 和KL 的等价性定理的内容及其证明。
􀁺 掌握NL 和KL 的等价性定理的使用。
􀁺 熟练掌握论域，解释，指派，项的值、公式的满足、真、永真的定义及其符号
表示。
􀁺 掌握公式（项）的值与约束变元取值的无关性。可代入性定理。命题代入实例
的性质。
􀁺 了解公式为假的等价性定义。
􀁺 熟练掌握可靠性、和谐性和完备性的内容及其证明。和谐公式集、极大和谐公
式集的概念及其性质。
􀁺 掌握一阶逻辑完备性证明的常量构作法——Henkin 方法。
 

第二十八章 消解原理*（可以不讲）
要点：命题公式与一阶谓词公式的消解
要求：
􀁺 熟练掌握文字、子句等概念
􀁺 熟练掌握命题公式的消解。
􀁺 熟练掌握Herbrand 定理
􀁺 掌握Robinson 合一算法
􀁺 掌握一阶谓词公式的消解