当前位置:主页 > 课后答案 > 计算机科学习题答案
面向计算机科学的数理逻辑:系统建模与推理(英文/第二版)

《面向计算机科学的数理逻辑:系统建模与推理(英文/第二版)》课后答案

  • 更新:2021-11-10
  • 大小:5.58 MB
  • 类别:计算机科学
  • 作者:Michael、Huth
  • 出版:机械工业出版社
  • 格式:PDF

  • 资源介绍
  • 学习心得
  • 相关内容

给大家带来的是关于计算机科学相关的课后习题答案,介绍了关于计算机科学、数理逻辑、系统建模、推理方面的内容,由崔鸿雪网友提供,本资源目前已被835人关注,高等院校计算机科学类教材综合评分为:7.1分。

书籍介绍

《面向计算机科学的数理逻辑系统建模与推理》是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 文献注释
  • 参考文献

资源获取

资源地址1:https://pan.baidu.com/s/19ztm4OeEsxovQMPYevGfDQ(密码:zplc)

相关资源

网友留言