《面向计算机科学的数理逻辑系统建模与推理》是2007年机械工业出版社出版的图书，作者是哈斯瑞安。本书适宜作为高等院校计算机及相关专业的数理逻辑/形式化方法课程的教材，也可供相关研究人员和专业人士参考。
本书对计算机科学方面的数理逻辑进行了综合介绍，涵盖命题逻辑、谓词逻辑、模态逻辑与代理、二叉判定图、模型检测和程序验证等内容。本书主要讨论有关软硬件规范和验证这一主题，反映了计算机科学中数理逻辑的新发展和实际需要。第2版新增了可满足性算法、L6wenheim—Skolem定理等，并介绍了Alloy语言和NuSMV工具等内容。
目录
- 出版者的话
- 专家指导委员会
- 译者序
- 第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 文献注释
- 参考文献
