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

完美实现逻辑与计算机的知识贯通，培养计算机学生数理逻辑思维

计算机是一种行为逻辑。计算机组件归根到底就是公式的逻辑实现方式，当这些组件被布尔信号激活时，就会计算其所表示公式的实际取值。软件也是一种逻辑体现。一个软件组件就是一种具有逻辑支撑的形式语言编写规范，某些软件组件其实就是代数公式。公式系统无论多么庞大复杂，也只是一些公式而已。
因此，学习计算机科学的人们可以从逻辑学习中获益，并且大多数计算机科学专业的学生在接受教育时都会接触到逻辑。这种接触通常以离散数学课程中的若干讲座和问题集的形式出现。学生看到的逻辑应用通常与传统数学的关系更加紧密，与计算机科学的关系则较为松散。即使对于“计算机科学中的离散数学”这样的课程而言，计算机科学部分也通常与编写解决传统数学问题的程序有关，而不是与计算机科学的概念有关。我们认为，如果计算机科学专业的学生对逻辑以及他们所选择的学习领域中的逻辑应用有更广泛、更严谨、更充分的认识，他们将会受益匪浅。因此，本书中的所有例子都来自计算机科学中的问题。
本书直接关注与计算机科学相关的中心主题。本书以逻辑为框架，对这些主题展开讨论，并将逻辑用于解决计算机科学领域的问题，包括硬件组件、软件组件、测试和验证以及算法分析。我们从归纳证明连接列表的软件组件的重要性质开始，然后继续验证许多其他软件和硬件组件的性质，而不是通过证明数列求和公式的方式来阐述数学归纳法。这是同样古老的数学归纳法，但是它呈现在计算机科学专业学生感兴趣的主题背景下。归纳逻辑属于前沿领域，数值代数的诀窍揭示了归纳逻辑的奥秘，许多归纳法的练习则需要以数学家深感兴趣的研究主题为基础进行讨论。
我们希望读者愿意付出大量努力，按顺序学习大学几十个课时的课程内容，理解计算机科学中的一些重要问题，并通过形式推理的方式尝试解决很多这样的问题。形式主义是本书的标语，甚至可以使用基于半自动化证明引擎ACL2的机械化逻辑。ACL2可以检查证明过程中的每个细节，有时可以补充传统数学证明，甚至严格数学证明留下的空白。
本书采用三种形式化表示法：传统的命题和谓词逻辑代数公式（偶尔有一些数值代数）表示法、数字电路图表示法以及在语法上类似于编程语言Lisp的ACL2表示法（ACL2被嵌入在可辅助生成一阶逻辑形式证明的机械化逻辑之中）。ACL2是一种数学符号，所有材料都可以通过传统的手工推理方式来理解，而无须将模型输入计算机系统。对于想要了解形式化操作的读者，本书还介绍了Proof Pad（简化版ACL2）环境。ACL2专家使用emacs或ACL2 Sedan作为界面，读者可以根据需要使用这些工具。本书还说明了Proof Pad框架中的过程，根据我们的经验，这对初学者而言也不是负担。在任何情况下，Proof Pad都足以支持对本书的学习。
我们选择了ACL2作为这本书的证明引擎，因为根据我们的判断，ACL2提供了比任何其他工具更容易理解的机械化逻辑证明形式。我们不指望每个读者都能成为有经验的ACL2用户，更不用说成为ACL2专家了。我们将ACL2引入讨论中，以显示软件和硬件工程师是如何从逻辑（包括机械化逻辑）中受益的。想要在大型项目中运用ACL2优势的读者，则需要在本书介绍的内容之外更为深入地了解ACL2或其他机械化逻辑。在前些年，我们在课堂上讲授逻辑时并未介绍机械化逻辑，然而根据经验，我们发现当使用能够检查证明和帮助处理细节的工具来支持这些形式化方法时，大多数学生都会感到更顺利且更有动力。
逻辑是本书的中心主题，但不是唯一的主题。对计算机科学更多主题感兴趣的读者会发现很多有用的资料。本书可以为认真学习计算机科学的学生和其他领域想要了解计算机科学的学生打下坚实的基础。本书的早期版本已被作者和其他讲师多次用作面向计算机科学以及其他专业学生的两门课程“计算机科学逻辑”和“计算机科学导论”的主要教材。本书也被用作计算机科学专业学生的离散数学课程的补充教材。本书在上述三个教学方面都发挥了很好的作用。
学习本书不需要大学预科课程或高中数学课程之外的预备知识。当然，如果了解一些高等代数知识会有所帮助，但不需要有几何、三角学或微积分方面的知识。编程经验也不是必需的，基于等式的方法可以为演示提供信息，让有或没有编程经验的人都可以学习本书内容。目标是证明自己已经知道这些知识的学生会惊讶地发现，其实自己以前并不知道这些知识，而那些背景知识较少的学生则从一开始就应当进行必要的努力。
学习本书的内容绝非易事。学生将需要进行很多艰苦的思考才能完成几十个练习，而且他们还需要再完成几十个练习才能掌握这些概念。仅仅看书是不够的，全书练习（总共超过180题）为学生提供了解决问题的机会。幸运的是，如果过往学生的学习体会是一个可靠的衡量标准，那么无论是从即刻满足感，还是从长期收益来看，学习本书都有回报。希望读者能够心情愉悦地阅读本书，并希望他们在后续做其他项目时发现自己所学的内容会对手头上的工作有所启发。
预备知识和章节相关性　在整个演示过程中，公式为严谨、形式化的方法提供了基础。理解等式只需要有高中代数基础，不需要其他预备知识。另外，有等式编程基础对理解本书十分有利。有关计算实践的章节更侧重于描述性，而不是严谨的形式化分析、讨论。读者可以对这些主题进行任意排列，并且可以延缓将挑战性概念引入等式和推理的进程。下图阐明了本书相关章节的关联路径。

致谢　作者想要感谢Caleb Eggensperger开发的Proof Pad环境，学生可以通过该环境获得机械化逻辑的早期经验，从而减轻了许多负担。感谢Carl Eastland、Dale Vaillancourt和Matthias Felleisen 建立了ACL2环境，其中一位作者在许多课程中都使用该环境，其中包括DoubleCheck——它是基于谓词的自动测试设备，是John Hughes和Koen Claessen基于QuickCheck（此类工具的祖先）中的理念而发明的，该设备后来被合并到Proof Pad中。我们感谢他们的开拓性工作。Qi Cheng在应用逻辑课程中使用了本书的原型版本，并提出了改进建议，使本书更加完善。作者还想要感谢1000多名学生，他们投身于本书的早期版本中，并提供了反馈。谢谢大家。

Rex Page和Ruben Gamboa
2018年1月

计算机科学及应用

数理逻辑之于计算机科学就像微积分之于物理。如果你真的想了解计算机科学，让这本书成为你的指南。
—— J. Strother Moore，得克萨斯大学奥斯汀分校荣休讲席教授

许多其他书将逻辑作为研究对象。相反，这本书以引人入胜的语言说明了逻辑如何在计算机科学中发挥作用，涵盖了从计算基础到程序设计、测试和验证的各种逻辑的使用。作为奖励，这本书使用了一个机械化逻辑系统，允许读者用形式化的方法进行实验。
——Veronica Gaspes，哈尔姆斯塔德大学副教授

你有没有想过逻辑和数学为什么会如此重要? Page和Gamboa通过生动地说明计算机科学如何基于逻辑进行工作的基本过程，带你踏上一段奇妙的学习旅程。你可以了解到数据结构、数字电路、排序、分片和MapReduce如何工作以及为什么工作，并且可以使用机械化逻辑证明这些工作的正确性。这是信息时代人们的基本知识。
—— Marco T. Morazán，西东大学教授

Page和Gamboa提供了一本优美、清晰、优雅的教材，向有抱负的软件开发人员介绍了软件背后的基础数学。基于本书开设一门课程将有助于学生进行学习。
—— Robby Findler，西北大学教授

作为思维的基本形式和基本规则，逻辑构成了人类思维和机器思维的共同基础，也是计算机科学与信息科学的理论基础。事实上，无论是计算机硬件还是计算机软件，它们都是一组逻辑组件的某种特定表现形式。具备严谨的逻辑思维能力对于计算机系统研发人员的重要性是毋庸置疑的。然而，逻辑思维能力的培养并不是一件很容易的事情，通常需要经历一定的理论学习和实际训练。目前，计算机专业的学生主要是通过离散数学等数学课程进行形式逻辑方面的学习，而不是直接面向计算机专业内容讨论计算机科学的基本逻辑，这使得学生接触到的逻辑知识与计算机科学的关系较为松散，不利于逻辑与计算机之间的知识贯通。本书可以很好地弥补这方面的不足。它以实际问题的求解为导向，对计算机科学的逻辑基础知识进行了比较系统的介绍、讨论和归纳，较好地实现了逻辑与计算机之间的知识贯通，可以有效地培育和提升读者的逻辑思维能力，使其能够在计算机逻辑方面获得比较系统的专业训练，从而能够更加高效地从事计算机软硬件产品的研发工作。本书的基本特点主要表现在如下三个方面：
第一，知识体系的组织结构突破了传统的数学框架，内容主要包括逻辑与等式、计算机算术、算法、计算实践四个部分，直接关注与计算机科学相关的逻辑主题，将逻辑用于解决计算机科学领域的问题，包括硬件组件、软件组件、测试和验证以及算法分析，逻辑知识与计算机知识的联系更加紧密，实现了两者的深度融合，特别适合用来对计算机专业人员进行系统性的逻辑训练。
第二，在可读性方面做了很好的设计，主要通过一些生动有趣的具体应用实例介绍逻辑知识和证明方法，能够有效地激发读者的学习兴趣，培养读者的逻辑思维和数学思维能力。例如，通过石头、剪刀、布这个简单的游戏深入浅出地阐述程序的基本结构和基于等式的程序模型，生动地解释了在基于等式的模型中，程序为何完全由基于操作数的数学函数组成，为何可以使用经典逻辑和传统代数公式来理解基于等式的程序。通过介绍深蓝计算机系统的基本工作原理来介绍归纳定义，使得读者能够清楚地认识到，对于计算机系统和逻辑系统而言，再复杂的行为通常也是从最初简单的行为演变而来，再复杂的理论通常也是建立在一些简单的基本原则基础之上。
第三，采用三种形式化表示法，即传统的逻辑代数公式表示法、数字电路图表示法以及ACL2表示法，使得学生可以借助软件工具比较容易地学习机械化逻辑的相关知识。本书使用ACL2作为逻辑证明引擎，ACL2提供了比任何其他工具更容易理解的机械化逻辑证明形式，通过事实生动地说明软件和硬件工程师可以如何从逻辑（包括机械化逻辑）中受益。当读者在检查证据和处理证明细节的很多方面得到ACL2软件工具的有效支持时，会非常开心并且更有学习动力。
本书内容丰富，文字表述清晰，实例讲解详细，图例直观形象，适合作为高等学校计算机、人工智能、大数据及相关专业的逻辑课程教材，也可供广大计算机爱好者、计算机及相关领域的科研人员和工程技术人员自学参考。
本书由汪荣贵、陈朗、汪雄飞共同翻译完成。感谢研究生孙旭、尹凯健、王维、张珉、李婧宇、修辉、雷辉、张法正、付炳光、张前进、叶萌、朱正发、汤明空、韩梦雅、邓韬、王静、龚毓秀、李明熹、董博文、麻可可、李懂、刘兵、江丹、王耀、杨尹、陈震、沈俊晖、黄智毅、禚天宇、黄姗姗、黄瀚慧等同学提供的帮助，感谢合肥工业大学、广东外语外贸大学、机械工业出版社的大力支持。
由于时间仓促，译文难免存在不妥之处，敬请读者不吝指正！

译者　　
2020年12月

出版者的话
译者序
前言
第一部分　逻辑与等式
第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