前言
第1章 导论
1.1 逻辑的基本概念和术语
1.2 逻辑学
1.2.1 概念与命题
1.2.2 推理论证
1.2.3 自然语言的歧义性与悖论
1.3 从亚里士多德经典逻辑到现代数理逻辑的演化
1.3.1 形式逻辑—推理形式与内容的分离
1.3.2 数理逻辑
1.4 计算机科学中的逻辑
1.4.1 逻辑是计算理论的天然基础
1.4.2 计算机科学技术领域的形式语言
1.4.3 形式证明与验证
第2章 离散数学基础
2.1 集合与集合代数
2.1.1 集合：概念、表示法和意义
2.1.2 子集
2.1.3 集合代数
2.2 关系和关系代数
2.2.1 笛卡儿积
2.2.2 关系
2.2.3 等价关系和划分
2.2.4 关系代数
2.2.5 关系的图示
2.3 函数
2.4 集合、关系、函数和谓词的联系与统一
2.4.1 关系和函数的统一
2.4.2 集合、关系、函数、谓词和布尔代数的统一
2.5 数学归纳法
2.6 集合上的序关系
2.6.1 偏序集
2.6.2 从已知的偏序集构造偏序集
2.6.3 偏序集间的函数
2.7 格、完全格和完全偏序集
2.7.1 偏序集的特殊子集和元素
2.7.2 格和完全格
2.7.3 保持上下确界的函数
2.7.4 塔斯基不动点理论
2.7.5 完全偏序集及不动点理论
2.8 集合的基数
第3章 朴素命题逻辑
3.1 引言
3.2 断言和连接词
3.3 连接词的真值函数和真值表
3.4 断言形式
3.4.1 断言形式的真值函数和真值表
3.4.2 断言形式的语法树
3.5 重言式和矛盾式
3.6 逻辑等价和逻辑蕴涵
3.6.1 逻辑等价
3.6.2 等价替换
3.6.3 逻辑蕴涵的性质
3.7 对偶式和断言范式
3.7.1 对偶式
3.7.2 断言形式的范式
3.7.3 充分连接词集合
3.7.4 子句形式
3.8 推理及推理的有效性
第4章 形式化命题逻辑
4.1 形式逻辑系统
4.2 形式命题逻辑系统L
4.3 L中的演绎推理
4.3.1 演绎定理
4.3.2 关于否定命题的证明与推演
4.4 形式系统L的有效性
4.5 相容性和L的充分性定理
第5章 朴素谓词逻辑
5.1 谓词和量词
5.1.1 谓词
5.1.2 变量、量词和函数
5.2 一阶形式语言
5.2.1 字母表
5.2.2 一阶语言的实例
5.2.3 合式公式
5.2.4 形式语言的语法层次结构
5.2.5 变元的自由与约束出现
5.2.6 换名和代换
5.3 解释
5.3.1 概念
5.3.2 赋值
5.3.3 合式公式可满足性
5.3.4 真值和模型
5.4 重言式和逻辑等价
5.4.1 重言式
5.4.2 逻辑有效的公式
5.4.3 逻辑蕴涵和逻辑等价
5.5 斯科伦定理
第6章 形式化谓词逻辑
6.1 形式系统KL
6.1.1 KL的有效性
6.1.2 KL的演绎定理
6.2 可证明等价和代换
6.3 KL的充分性定理
6.3.1 KL的扩展
6.3.2 充分性定理的证明
6.4 模型
6.5 范式
6.5.1 量词辖域的变换
6.5.2 前束范式
6.5.3 子句形式
第7章 数学系统
7.1 带等词的一阶系统
7.2 公理化群论
7.2.1 群的非形式定义
7.2.2 形式化群论
7.3 公理化布尔代数
7.4 形式化算术
7.4.1 算术的形式化
7.4.2 与皮亚诺算术的关系
7.4.3 形式化算术的模型及完备性问题
7.5 公理集合论
7.5.1 ZF公理系统
7.5.2 ZF公理系统的模型
7.6 相容性和模型之间的关系
第8章 程序设计理论导引
8.1 计算、计算机和计算机程序
8.1.1 可计算性和计算机
8.1.2 程序语法的非形式定义
8.1.3 程序的非形式语义
8.2 程序语言的形式语法
8.3 程序语言的操作语义
8.3.1 栈-状态-控制抽象机解释语义
8.3.2 基于操作语义的程序分析和验证
8.3.3 结构化操作语义
8.3.4 完整的结构化操作语义
8.4 程序语言的指称语义
8.4.1 基本思想和技术
8.4.2 核心问题
8.4.3 Mini的指称语义定义
8.5 指称语义和操作语义的一致性
8.6 程序语言的公理语义
8.6.1 非形式霍尔逻辑
8.6.2 霍尔逻辑
8.6.3 霍尔逻辑可靠性和完全性
8.7 抽象数据类型
参考文献
索引
展开
