计算机科学的逻辑基础

图书标准信息

• 作者 [美]雷克斯·佩奇（Rex Page）；[美]鲁本·冈
• 出版社 机械工业出版社
• 出版时间 2021-06
• 版次 1
• ISBN 9787111682226
• 定价 99.00元
• 装帧 平装
• 开本 16开
• 纸张 胶版纸
• 字数 400千字

【内容简介】

介绍如何将谓词逻辑应用于软件和数字电路的测试和验证，重点是应用而不是理论。

【目录】

出版者的话

译者序

前言

第一部分　逻辑与等式

第1章　计算机系统：原理简单，行为复杂  2

1.1　硬件与软件  2

1.2　程序的结构  4

1.3　深蓝与归纳定义  7

习题  10

第2章　布尔公式和等式  11

2.1　利用等式推理  11

习题  13

2.2　布尔等式  13

习题  19

2.3　布尔公式  19

习题  22

2.4　数字电路  23

习题  26

2.5　演绎推理  27

习题  36

2.6　谓词和量词  37

习题  40

2.7　量化谓词的推理  40

习题  47

2.8　布尔模型  47

习题  52

2.9　谓词和量词的一般模型  52

第3章　软件测试和前缀法  55

习题  59

第4章　数学归纳  61

4.1　数学对象列表  61

习题  65

4.2　数学归纳法  65

习题  71

4.3　Defun：ACL2中运算符的定义  71

4.4　连接、前缀和后缀  72

习题  77

第5章　机械化逻辑  78

5.1　ACL2定理与证明  78

5.2　使用已证的定理库  80

习题  80

5.3　约束定理  81

习题  83

5.4　辅助机械化逻辑工作  83

习题  86

5.5　自动化证明及其做不到的事  86

习题  92

第二部分　计算机算术

第6章　二进制数字  94

6.1　数和数字  94

习题  98

6.2　从数字到数  99

习题  102

6.3　二进制数字  103

习题  104

第7章　加法器  106

7.1　数字相加  106

习题  106

7.2　一位二进制数字加法电路  106

7.3　两位二进制数字加法电路  109

习题  110

7.4　w位二进制数字加法  110

习题  113

7.5　负数的数字  114

习题  116

第8章　乘法器和大数算法  118

8.1　大数加法器  118

习题  121

8.2　移位相加乘法器  121

习题  124

第三部分　算法

第9章　多路复用器和解复用器  126

9.1　多路复用器  126

习题  129

9.2　解复用器  129

习题  131

第10章　排序  132

10.1　插入排序  132

习题  135

10.2　保序合并  135

习题  137

10.3　归并排序  137

习题  139

10.4　排序算法分析  139

10.4.1　计算步骤的计数  139

习题  141

10.4.2　计算解复用的步数  141

习题  142

10.4.3　计算归并的步数  143

习题  144

10.4.4　计算归并排序的步数  144

习题  147

10.4.5　计算插入排序的步数  147

习题  149

第11章　搜索树  150

11.1　查找事物  150

11.2　平衡二叉树  152

11.3　搜索树的表示  154

11.4　有序搜索树  155

习题  156

11.5　平衡搜索树  156

习题  157

11.6　搜索树中插入新项目  157

习题  159

11.7　顺序插入  159

习题  163

11.8　双旋转  164

习题  167

11.9　快速插入  167

习题  169

第12章　哈希表  170

12.1　列表和数组  170

12.2　哈希运算符  172

习题  177

12.3　一些应用  178

第四部分　计算实践

第13章　Facebook分片技术  182

13.1　技术挑战  182

13.2　权宜之计  183

13.2.1　缓存  183

13.2.2　分片  184

13.3　Cassandra的解决方案  185

13.4　小结  186

第14章　MapReduce的并行计算  187

14.1　水平扩展和垂直扩展  187

14.2　MapReduce的策略  188

14.3　基于MapReduce的数据挖掘  191

14.4　小结  195

第15章　计算机艺术创作  196

15.1　在计算机中表示图像  196

15.2　随机生成图像  198

15.3　生成目标图像  201

索引  203