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