Assuming no previous study in logic, this informal yet rigorous text covers the material of a standard undergraduate first course in mathematical logic, using natural deduction and leading up to the completeness theorem for first-order logic. At each stage of the text, the reader is given an intuition based on standard mathematical practice, which is subsequently developed with clean formal mathematics. Alongside the practical examples, readers learn what can and can't be calculated; for example the correctness of a derivation proving a given sequent can be tested mechanically, but there is no general mechanical test for the existence of a derivation proving the given sequent. The undecidability results are proved rigorously in an optional final chapter, assuming Matiyasevich's theorem characterising the computably enumerable relations. Rigorous proofs of the adequacy and completeness proofs of the relevant logics are provided, with careful attention to the languages involved. Optional sections discuss the classification of mathematical structures by first-order theories; the required theory of cardinality is developed from scratch. Throughout the book there are notes on historical aspects of the material, and connections with linguistics and computer science, and the discussion of syntax and semantics is influenced by modern linguistic approaches. Two basic themes in recent cognitive science studies of actual human reasoning are also introduced. Including extensive exercises and selected solutions, this text is ideal for students in Logic, Mathematics, Philosophy, and Computer Science.

本书采用将逻辑设计与计算机设计原理结合在一起的方法，为广大读者提供了学习逻辑设计、数字系统设计和计算机设计的基础知识。从1997年第1版开始，作者就不断对其进行丰富和修改，最新的第4版包含了相关研究领域和产业的最新发展状况。从基础理论到系统方法、从实用技术到现代化工具，本书从各个方面向读者展示了一个自然而流畅、高效并富有哲理的数字电路设计世界。 第4版除了提供完整的数字和计算机设计内容之外，还特别强调基本原理为现代设计服务。全书以清晰的实例解释和逐步延伸的设计来帮助读者理解内容，实例涵盖了从简单的组合逻辑应用到在一个RISC核上构建一个CISC结构，更加重视培养读者在计算机辅助设计、问题形式化、解决方案验证以及解决问题技巧方面的能力。 本书的补充材料和教辅资源丰富，包括部分习题答案、PPT、VHDL和Verilog代码，及补充阅读材料等，方便教师教学和读者自学。 本版更新内容：  新增60个“现实世界”的例子和问题。  新增和修改了40%的习题。  重新调整和组织了内容以适应不同的课程大纲。 技术内容的更新包括：  简要介绍嵌入式系统。  解释了在Espresso中实际使用的计算机辅助逻辑优化方法。  用液晶显示屏例子更换CRT显示器例子。  包括多CPU微处理器在内的体系结构方面的一些创新。 【译者序】 如今我们生活在信息时代。试想，如果没有了网络、电脑、手机和电视，世界会变得怎样？答案一定是世界将变得暗淡无光，甚至是悲惨的！数字电路与计算机技术作为其他技术的重要基础之一，成就了当今人们高效有序、丰富多彩的工作与生活。从发明晶体管和集成电路到现在，数字电路和数字系统设计技术已经红红火火地走过了半个多世纪，计算机技术更是在最近三十年得到了跳跃式的发展。人们对未来充满着更多美好的期望，数字电路与计算机必将承载着这一切向更广范围、更高水准延伸与发展。 从1997年至今，本书的英文版已经发行了4个版本，均受到了读者的广泛好评。第4版除了为读者提供学习逻辑设计、数字系统设计和计算机设计的基础知识之外，还包含有相关研究领域和行业的最新发展状况。从基础理论到系统方法、从实用技术到现代化工具，本书从各个方面向读者展示了一个自然而流畅、高效并富有哲理的数字电路设计世界。 本书以一台通用计算机为线索，由浅入深地讲解了逻辑设计、数字系统设计和计算机设计。其中，第1章到第5章为逻辑设计，包括数字系统与信息、组合逻辑电路及其设计、算术功能块与硬件描述语言，以及时序电路；第6章到第8章为数字系统设计，包括可选的设计话题：数据通路、算术逻辑单元、移位寄存器、一个简单计算机的结构、单周期硬连线控制、多周期硬连线控制等，寄存器与寄存器传输，以及存储器基础；第9章到第13章为计算机设计，包括计算机设计基础、指令集结构、RISC与CISC中央处理器、输入输出与通信，以及存储系统。书中附有60个大部分来自现代日常生活中产品设计的真实例子和问题，可以激发读者的学习兴趣。配套网站（http://www.prenhall.com/mano）提供了大量的辅助信息，包括教师手册、补充读物、所有例子的VHDL和Verilog源文件、有关工具及网站的链接和习题解答等。从其编排可以清楚地看出，本书不仅可以作为计算机科学、计算机工程、电子技术、机电一体化等专业学生学习硬件的一本绝佳教材，也可以作为弱电类工程师和计算机科学工作者的理想参考书籍。 本书由袁晓坊翻译第1、12章，何海珍翻译第2、3章，凌纯清翻译第4、6章，王伟征翻译第5章，周颖波翻译第7章，张玲翻译第8、13章，袁文澹翻译第9、10章，刘铁桥翻译第11章。邝继顺参加了第2、9章的翻译，并对全部译文进行了审校与润饰。由于译者水平有限，译文中疏漏和错误在所难免，欢迎广大读者批评指正。 译者 2011年12月于湖南长沙 【前言】 本书的目的是为广大读者提供学习逻辑设计、数字系统设计和计算机设计的基础知识，本书第4版包含了近十年与课程内容相关方面的最新发展情况。从1997年的第1版开始，作者就不断对其进行修改，提供了一种独一无二的将逻辑设计与计算机设计原理结合在一起的方法，并特别强调硬件。过去几年，教材一直紧跟工业的发展趋势，增加了新的材料如硬件描述语言，删除或者弱化了某些正变得不太重要的内容，修改了某些内容以反映计算机技术和计算机辅助设计所发生的变化。 在第4版中，我们不仅关注如何教好这门课，而且也关注工业发展的趋势。大部分来自现代日常生活中产品设计的60个“现实世界”的例子和问题，可以激发读者的学习兴趣，并为其提供实践的解决方案。在章节组织方面的修改可以使教师更容易为学生量身定做所要学习的内容，同时适用于电气与计算机工程专业和计算机科学专业的读者。 在这个版本中，我们首先将原来第3章中关于设计的一般性介绍和原来第4章中的功能模块结合在一起形成新的第3章。原来第3章中关于设计的一些科学内容现在作为必备的基础分布在多个章节中，并附有例子和说明。用于组合电路和算术电路的硬件描述语言放到第4章，以便平衡章节篇幅。过去第3章中有关技术方面的内容，包括时序、可编程逻辑出现在新的第6章中，教师可以根据课程教学大纲进行适当的选择和讲解。经过重新编排的第6章，允许那些对相关技术要求较少的人更早地接触时序电路，并为一些专题提供更为广泛的、必备的背景知识。况且，把技术性话题放在数字系统设计中比放在较早介绍的基本逻辑设计中更加合适。第6章还包含一些CMOS电路以及系统之间进行异步交互的新的信息，包括输入同步和亚稳态。 原来的第8章连同用来对复杂时序电路和控制单元进行流水线式设计的算法状态机（ASM）被取消了，第8章里面的概念被分散到第5章和第7章中。一种新的状态机图形表示代替了ASM。这个状态机图是在传统状态图的基础上建模而成的，它能生动地用图形的方式表示出用硬件描述语言进行建模所具有的自然的灵活性。还有，在第7章，我们把合成数据通路和控制单元的设计过程进行了形式化，并举例给予了说明。 本书第4版除了提供完整的数字和计算机设计内容之外，还特别强调基本原理为现代设计服务。从简单的组合逻辑应用到在一个RISC核上构建一个CISC结构，多个例子的清晰解释和渐进式的设计可以诠释书中内容。完整的传统内容包括计算机辅助设计、问题形式化、解决方案验证，以及解决问题的技能的培养，而灵活性则体现在可选的逻辑设计、数字系统设计和计算机设计以及硬件描述语言的相关内容中。第4版除了组织和内容方面的这些改变之外，其他方面的改变还有：（1）对嵌入式系统的简要介绍；（2）解释了在Espresso中实际使用的计算机辅助逻辑优化方法；（3）用液晶显示屏例子更换CRT显示器例子；（4）包括多CPU微处理器在内的体系结构方面的一些创新。 经过这些修订，书本第1章到第5章讲解逻辑设计，第6章到第8章研究数字系统设计，第9章到第13章关注计算机设计。这样的编排可以在逐渐地、自底向上地完成了各种函数设计，并将其应用到后续章节自顶向下的计算机设计中之后，为读者提供牢固的数字系统设计的基础。下面是各章相关内容的概括。 第1章——数字系统与信息。这一章介绍数字计算机、嵌入式系统和包括数字、算术运算及编码在内的信息表示。 第2章——组合逻辑电路。这一章研究门电路和它们的类型，以及设计和优化的基本方法。概念包括布尔代数、代数优化和卡诺图优化、Espresso算法作为实用的CAD优化工具以及多级优化。 第3章——组合逻辑电路的设计。这一章以一个现代逻辑设计过程的概述开始。设计过程的详细步骤包括问题形式化、逻辑优化、到与非门和或非门的工艺映射，验证也包含在组合逻辑设计的实例中。另外，这一章还包含函数和组合设计的模块构建，包括使能和输入定值、译码、编码、代码转换、选择、分配和它们的实现。 第4章——算术功能块与硬件描述语言。这一章讲解算术功能块和它们的实现。除算术运算如加法、减法和自增用数字来表示之外，还对自减、填充、扩展和移位进行了描述和实现。介绍了综合过程和硬件描述语言。Verilog和VHDL从第3章起就用来描述组合逻辑，从这一章起用来描述算术运算逻辑。 第5章——时序电路。这一章包含时序电路分析和设计。锁存器、主从触发器、边沿触发器都有涉及，并着重讲解了D触发器，而其他类型的触发器（SR、JK与T）在现代设计中用得比较少，只是简要地说明了一下。本章的重点是状态机图和状态表的形式化表示。一个时序电路完整的设计过程包括规格说明、形式化、状态分配、触发器输入和输出函数确定、优化、工艺映射以及验证。时序电路通常都太复杂而不能用传统的状态图来表示，但可以用状态机图模型来表示，这一章通过两个现实世界的例子来阐述和说明这一观点。这一章的最后用VHDL和Verilog描述了一个触发器和一个时序电路。 第6章——选择的设计主题。这一章介绍的内容侧重于底层技术的各个方面，包括MOS晶体管和CMOS电路、门时延和定时、组合电路和时序电路、电路之间的异步交互作用，以及可编程逻辑技术。其中，异步交互部分包括异步输入的同步和亚稳态，可编程逻辑包含只读存储器、可编程逻辑阵列和可编程阵列逻辑。 第7章——寄存器与寄存器传输。这一章讲解寄存器和它们的应用。移位寄存器和计数器的设计基于第3章和第4章讲解的触发器和某些函数及其实现的组合，只有行波计数器作为一个全新的概念加以介绍。讨论了寄存器传输的并行和串行方式，如何权衡时间与空间开销，其中有一节侧重于能执行多种运算的多功能寄存器的寄存器单元设计。数据通路和控制单元的协同过程使用了寄存器传输语言和状态机图，并且用两个现实世界的例子对其进行了解释，对所选的寄存器类型也用Verilog和VHDL语言进行了描述。 第8章——存储器基础。这一章介绍静态随机访问存储器（SRAM）和动态随机访问存储器（DRAM），以及基本存储器系统，还简单地介绍了静态随机访问存储器的各种不同类型。 第9章——计算机设计基础。这一章包括寄存器文件、功能单元、数据通路和两种简单计算机，包括一种单周期计算机和一种多周期计算机。重点在于数据通路和控制单元设计的形式化概念，以及用来设计具有特定指令和指令集的单周期和多周期计算机。 第10章——指令集结构。介绍指令集结构的相关问题，包括地址计算、寻址模式、指令结构和类型。讲解浮点数表示法和浮点运算，以及程序控制方法，包括过程调用与中断。 第11章——RISC和CISC中央处理单元。这一章包含一些高性能处理器的概念，如流水式RISC和CISC处理单元。通过将一个微编码硬件加到一个修改了的RISC处理单元上，CISC处理单元可以使用RISC的流水线来执行CISC指令集，这是当今CISC处理单元使用的一种方法。除此之外，还介绍了高性能CPU在概念和结构方面的创新，其中包括两个多CPU微处理器的例子。 第12章——输入输出与通信。这一章讲解如何在CPU和内存之间、输入输出接口和外围设备之间进行数据传送。讨论了键盘、液晶显示器（LCD）、硬盘驱动器等外部设备和键盘接口，以及包括通用串行总线（USB）在内的串行通信和中断系统的实现。 第13章——存储系统。特别重点关注存储器的分层。引入了“访问的局部性”的概念，并通过高速缓存和内存之间、内存和硬盘之间的关系对其进行了详细讲解。分析了高速缓存设计的各种参数。存储器管理重点关注分页管理和支持虚拟存储的转换后援缓冲器。 除了教材本身之外，还提供了一个配套网站（http://www.prenhall.com/mano）和一本教师手册。配套网站的内容包括以下几个方面：1）阅读补充材料，包括一些新材料和先前版本中删除掉的部分内容；2）所有例子的VHDL和Verilog源文件；3）连接到用于FPGA设计和HDL模拟的计算机辅助设计工具的链接；4）全书大约1/3习题的答案；5）勘误表；6）第1章到第9章的幻灯片；7）书中复杂图表的原件；8）为学生和教师提供新信息、更新和更正内容的网站消息。我们鼓励教师定期查看网站上的信息以便了解网站的变化。教师手册包括书的使用建议以及所有习题的答案。从Prentice Hall到学校，每一个使用这本书上课的教师都有权限在线访问这本手册。使用建议还提供了在各种不同课程教学大纲下使用该教材的重要的详细信息。 由于本书覆盖逻辑和计算机设计的面很广，作为大二到大三学生的课程它有几个不同的目的。从第1章到第10章，去掉可选的内容外，其余部分可以作为计算机科学、计算机工程、电气工程或一般工程专业的学生一个学期学习硬件的课程。从第1章到第5章，或许再加上第6章到第8章一些可选部分是对逻辑设计的一个基本介绍，对电气工程和计算机工程专业的学生来说，这些内容只要一个季度的学习时间就够了。一个学期学完第1章到第8章的全部内容，将会学到更为强大、更加先进的逻辑设计方法。整本书在两个季度的时间内，可以为计算机工程和计算机科学专业的学生提供逻辑和计算机设计的基础知识。本书的全部内容再加上适当的补充材料或实验环节，可以作为两个学期学习逻辑设计和计算机结构的课程。由于取材广泛，并且处理得当，本书还是工程师和计算机科学工作者自学的理想书籍。最后，配套网站上提供的补充读物对实现这些不同的目标来说都是有益的。 在第4版的准备期间，我们征求了许多使用过本书前面几版的教师的意见，对超过50位教师进行了广泛的关于第3版内容及其使用情况的调查。另外，Vanderbilt大学的Bharat Bhuva教授和San Jose州立大学的Donald Hung教授，通过对第3版撰写评论提供了有用的反馈意见。我们非常感谢所有教师在第4版准备过程中的积极参与以及他们的建设性意见，特别感谢Katherine Compton、Mikko Lipasti、Kewal Saluja和Leon Shohet教授以及威斯康星大学麦迪逊分校电气与计算机工程系的Michael Morrow教师委员会。在他们提供的大量评论和建议的基础上，通过与第二作者的重点讨论，我们对原定第4版的内容进行了重大调整。我们还要感谢教师和学生对第3版提出的修正，尤其是Dordt大学的Douglas De Boer教授的修改意见。特别感谢威斯康星大学麦迪逊分校的Divya Jhalani，她对教师手册和网站上新给出的习题进行了解答。我们感谢所有在Prentice Hall或其他地方的工作人员对出版所做出的努力。特别要感谢Mike McDonald编辑的指导、鼓励和支持，制作编辑Dan Sandin和Irvwin Zucker对本书出版所做的富有成效的工作，以及Bob Lentz的一丝不苟的编辑工作。最后，特别感谢Val Kime对第4版整个过程持久的耐心和理解。 M.Morris Mano Charles R.Kime

《普通高等学校十一五规划教材•数理逻辑(第2版)》内容分两部分：第一部分属数理逻辑基础，包含命题演算与谓词演算的基本知识。第二部分为形式算术与Godel不完备性定理。《普通高等学校十一五规划教材•数理逻辑(第2版)》对Godel第一不完备性定理、Godel-Rosser定理、Tarski定理及形式算术的不可判定性定理等都提供了完整的证明。结合对Church论题与Turing论题的介绍，对这些定理的意义进行了讨论。书中还提出了Godel第二不完备性定理的一种易证形式。 《普通高等学校十一五规划教材•数理逻辑(第2版)》可用作计算机专业研究生或高年级本科生教材，并可供数学、哲学、逻辑等专业研究及教学人员参考。

译自: Logic for mathematicans/A. G. Hamilton. -- 剑桥大学出版社, 1978

Recent years have seen the development of powerful tools for verifying hardware and software systems, as companies worldwide realise the need for improved means of validating their products. There is increasing demand for training in basic methods in formal reasoning so that students can gain proficiency in logic-based verification methods. The second edition of this successful textbook addresses both those requirements, by continuing to provide a clear introduction to formal reasoning which is both relevant to the needs of modern computer science and rigorous enough for practical application. Improvements to the first edition have been made throughout, with extra and expanded sections on SAT solvers, existential/universal second-order logic, micro-models, programming by contract and total correctness. The coverage of model-checking has been substantially updated. Further exercises have been added. Internet support for the book includes worked solutions for all exercises for teachers, and model solutions to some exercises for students.