形式化方法:理论及应用

前言 第1章 基础知识 1.1 集合 1.2 关系与映射 1.3 上下文无关文法 1.4 归纳法 1.5 归纳定义 1.6 实现 第2章 命题逻辑 2.1 语法 2.2 证明系统 2.3 构造逻辑 2.4 语义系统 2.5 可靠性和完备性定理 2.6 可判定性 2.7 命题逻辑的实现 第3章 布尔可满足性 3.1 布尔可满足性 3.2 合取范式 3.3 决议与传播 3.4 DPLL算法 3.5 实现 第4章 谓词逻辑 4.1 命题的内部结构 4.2 语法 4.3 证明系统 4.4 语义系统 4.5 可靠性和完备性 4.6 可判定性 4.7 实现 第5章 等式与未解释函数理论 5.1 可满足性模理论 5.2 等式与未解释函数理论 5.3 基本性质 5.4 判定算法 5.5 实现 5.6 应用 第6章 线性算术理论 6.1 语法 6.2 高斯消元 6.3 傅里叶-莫茨金消元 6.4 单纯形法 6.5 分支定界法 6.6 减法逻辑 6.7 实现 6.8 应用 第7章 数据结构理论 7.1 位向量 7.2 数组 7.3 指针