面向计算机科学的数理逻辑系统建模与推理（原书第2版）

出版者的话
专家指导委员会
译者序
第1版序
第2版前言
第1章 命题逻辑
1．1 判断语句
1．2 自然演绎
1．2．1 自然演绎规则
1．2．2 派生规则
1．2．3 自然演绎总结
1．2．4 逻辑等价
1．2．5 侧记：反证法
1．3 作为形式语言的命题逻辑
1．4 命题逻辑的语义
1．4．1 逻辑连接词的含义
1．4．2 数学归纳法
1．4．3 命题逻辑的合理性
1．4．4 命题逻辑的完备性
1．5 范式
1．5．1 语义等价、满足性和有效性
1．5．2 合取范式和有效性
1．5．3 霍恩子句和可满足性
1．6 SAT求解机
1．6．1 线性求解机
1．6．2 三次求解机
1．7 习题
1．8 文献注释
第2章 谓词逻辑
2．1 我们需要更丰富的语言
2．2 作为形式语言的谓词逻辑
2．2．1 项
2．2．2 公式
2．2．3 自由变量和约束变量
2．2．4 代换
2．3 谓词逻辑的证明论
2．3．1 自然演绎规则
2．3．2 量词的等价
2．4 谓词逻辑的语义
2．4．1 模型
2．4．2 语义推导
2．4．3 相等的语义
2．5 谓词逻辑的不可判定性
2．6 谓词逻辑的表达能力
2．6．1 存在式二阶逻辑
2．6．2 全称式二阶逻辑
2．7 软件的微观模型
2．7．1 状态机
2．7．2 Alma重观
2．7．3 软件的微模型

2．8 习题
2．9 文献注释
第3章 通过模型检测进行验证
3．1 验证的动机
3．2 线性时态逻辑
3．2．1 LTL的语法
3．2．2 LTL的语义
3．2．3 规范的实际模式
3．2．4 LTL公式之间的重要等价
3．2．5 LTL的适当连接词集
3．3 模型检测：系统、工具和性质
3．3．1 例：互斥
3．3．2 NuSMV模型检测器
3．3．3 运行NuSMV
3．3．4 重温互斥
3．3．5 摆渡者难题
3．3．6 交错位协议
3．4 分支时间逻辑
3．4．1 CTL的语法
3．4．2 计算树逻辑的语义
3．4．3 规范的实际模式
3．4．4 CTL公式间的重要等价
3．4．5 CTL连接词的适当集
3．5 CTL*与LTL和CTL的表达能力
3．5．1 CTL中时态公式的布尔组合
3．5．2 LTL中的过去算子
3．6 模型检测算法
3．6．1 CTL模型检测算法
3．6．2 具有公平性的CTL模型检测
3．6．3 LTL模型检测算法
3．7 CTL的不动点特征
3．7．1 单调函数
3．7．2 SATEG的正确性
3．7．3 SATEU的正确性
3．8 习题
3．9 文献注释
第4章 程序验证
4．1 为什么要规范和验证编码
4．2 软件验证的一种框架
4．2．1 一种核心程序设计语言
4．2．2 霍尔三元组
4．2．3 部分正确性和完全正确性
4．2．4 程序变量和逻辑变量
4．3 部分正确性的证明演算
4．3．1 证明规则
4．3．2 证明布景
4．3．3 案例研究：最小和截段
4．4 完全正确性的证明演算
4．5 合同编程
4．6 习题

4．7 文献注释
第5章 模态逻辑与代理
5．1 真值的模式
5．2 基本模态逻辑
5．2．1 语法
5．2．2 语义
5．3 逻辑工程
5．3．1 有效公式储备
5．3．2 可达关系的重要性质
5．3．3 对应理论
5．3．4 一些模态逻辑
5．4 自然演绎
5．5 多代理系统中的知识推理
5．5．1 一些例子
5．5．2 模态逻辑KT45n
5．5．3 KT45n的自然演绎
5．5．4 例子的形式化
5．6 习题
5．7 文献注释
第6章 二叉判定图
6．1 布尔函数的表示
6．1．1 命题公式和真值表
6．1．2 二叉判定图
6．1．3 有序BDD
6．2 简约OBDD的算法
6．2．1 算法reduce
6．2．2 算法apply
6．2．3 算法res七rict
6．2．4 算法exis七s
6．2．5 OBDD的评价
6．3 符号模型检测
6．3．1 表示状态集合的子集
6．3．2 表示迁移关系
6．3．3 实现函数pre3和preν
6．3．4 综合OBDD
6．4 关系μ演算
6．4．1 语法和语义
6．4．2 对CTL模型及规范说明的编码
6．5 习题
6．6 文献注释
参考文献