![面向计算机科学的数理逻辑：系统建模与推理（英文版·第2版）[按需印刷]](http://images.china-pub.com/ebook20001-25000/24321/zcover.jpg)
（已有17条评价）基本信息
- 原书名：Logic in Computer Science : Modelling and Reasoning about Systems,Second Edition
- 原出版社： Cambridge University Press
内容简介
书籍
计算机书籍
数理逻辑是计算机科学的基础之一，在模型与系统的规约与验证等方面有着广泛的应用。随着当今软硬件产品(电路、程序和通信协议等)日趋复杂，数理逻辑已经成为越来越多设计开发人员的日常工具。
本书适合作为高等院校计算机及相关专业的数理逻辑／形式化方法课程教材，涵盖了命题逻辑、谓词逻辑、模态逻辑与Agent、二元决策图、模型检查和程序验证等内容。与传统数理逻辑教科书相比，它的主要特色就是紧紧围绕软硬件规约和验证这一主题，反映了计算机科学中数理逻辑的新发展和实际需要。第2版新增了可满足性(SAT)算法、紧致性理论和Lowenheim-Skolem定理，并介绍了Alloy语言和NuSMV工具。
本书自出版以来受到广泛好评，已经被包括美国普林斯顿大学、卡内基—梅隆大学、英国剑桥大学、德国汉堡大学、加拿大多伦多大学、荷兰Vrije大学、印度理工学院在内的多个国家几十所高校采纳为教材。
计算机书籍
数理逻辑是计算机科学的基础之一，在模型与系统的规约与验证等方面有着广泛的应用。随着当今软硬件产品(电路、程序和通信协议等)日趋复杂，数理逻辑已经成为越来越多设计开发人员的日常工具。
本书适合作为高等院校计算机及相关专业的数理逻辑／形式化方法课程教材，涵盖了命题逻辑、谓词逻辑、模态逻辑与Agent、二元决策图、模型检查和程序验证等内容。与传统数理逻辑教科书相比，它的主要特色就是紧紧围绕软硬件规约和验证这一主题，反映了计算机科学中数理逻辑的新发展和实际需要。第2版新增了可满足性(SAT)算法、紧致性理论和Lowenheim-Skolem定理，并介绍了Alloy语言和NuSMV工具。
本书自出版以来受到广泛好评，已经被包括美国普林斯顿大学、卡内基—梅隆大学、英国剑桥大学、德国汉堡大学、加拿大多伦多大学、荷兰Vrije大学、印度理工学院在内的多个国家几十所高校采纳为教材。
作译者
Michael Huth 伦敦帝国学院计算系高级讲师，研究方向包括模型检测与抽象、程序分析和模型检测中有序结构的应用等。
Mark Ryan 伯明翰大学计算机科学学院高级讲师，主要研究方向包括模型检测、时序及模态逻辑和非单调推理等。
Mark Ryan 伯明翰大学计算机科学学院高级讲师，主要研究方向包括模型检测、时序及模态逻辑和非单调推理等。
目录
Foreword to the first edition
Preface to the second edition
Acknowledgements
1 Propositional logic
1.1 Declarative sentences
1.2 Natural deduction
1.2.1 Rules for natural deduction
1.2.2 Derived rules
1.2.3 Natural deduction in summary
1.2.4 Provable equivalence
1.2.5 An aside: proof by contradiction
1.3 Propositional logic as a formal language
1.4 Semantics of propositional logic
1.4.1 The meaning of logical connectives
1.4.2 Mathematical induction
1.4.3 Soundness of propositional logic
1.4.4 Completeness of propositional logic
1.5 Normal forms
1.5.1 Semantic equivalence, satisfiability and validity
1.5.2 Conjunctive normal forms and validity
Preface to the second edition
Acknowledgements
1 Propositional logic
1.1 Declarative sentences
1.2 Natural deduction
1.2.1 Rules for natural deduction
1.2.2 Derived rules
1.2.3 Natural deduction in summary
1.2.4 Provable equivalence
1.2.5 An aside: proof by contradiction
1.3 Propositional logic as a formal language
1.4 Semantics of propositional logic
1.4.1 The meaning of logical connectives
1.4.2 Mathematical induction
1.4.3 Soundness of propositional logic
1.4.4 Completeness of propositional logic
1.5 Normal forms
1.5.1 Semantic equivalence, satisfiability and validity
1.5.2 Conjunctive normal forms and validity
译者序
文艺复兴以降，源远流长的科学精神和逐步形成的学术规范，使西方国家在自然科学的各个领域取得了垄断性的优势；也正是这样的传统，使美国在信息技术发展的六十多年间名家辈出、独领风骚。在商业化的进程中，美国的产业界与教育界越来越紧密地结合，计算机学科中的许多泰山北斗同时身处科研和教学的最前线，由此而产生的经典科学著作，不仅擘划了研究的范畴，还揭橥了学术的源变，既遵循学术规范，又自有学者个性，其价值并不会因年月的流逝而减退。
近年，在全球信息化大潮的推动下，我国的计算机产业发展迅猛，对专业人才的需求日益迫切。这对计算机教育界和出版界都既是机遇，也是挑战；而专业教材的建设在教育战略上显得举足轻重。在我国信息技术发展时间较短、从业人员较少的现状下，美国等发达国家在其计算机科学发展的几十年间积淀的经典教材仍有许多值得借鉴之处。因此，引进一批国外优秀计算机教材将对我国计算机教育事业的发展起积极的推动作用，也是与世界接轨、建设真正的世界一流大学的必由之路。
机械工业出版社华章图文信息有限公司较早意识到"出版要为教育服务"。自1998年开始，华章公司就将工作重点放在了遴选、移译国外优秀教材上。经过几年的不懈努力，我们与Prentice Hall，Addison-Wesley，McGraw-Hill，MorganKaufmann等世界著名出版公司建立了良好的合作关系，从它们现有的数百种教材中甄选出Tanenbaum，Stroustrup，Kernighan，JimGray等大师名家的一批经典作品，以"计算机科学丛书"为总称出版，供读者学习、研究及庋藏。大理石纹理的封面，也正体现了这套丛书的品位和格调。
"计算机科学丛书"的出版工作得到了国内外学者的鼎力襄助，国内的专家不仅提供了中肯的选题指导，还不辞劳苦地担任了翻译和审校的工作；而原书的作者也相当关注其作品在中国的传播，有的还专诚为其书的中译本作序。迄今，"计算机科学丛书"已经出版了近百个品种，这些书籍在读者中树立了良好的口碑，并被许多高校采用为正式教材和参考书籍，为进一步推广与发展打下了坚实的基础。
随着学科建设的初步完善和教材改革的逐渐深化，教育界对国外计算机教材的需求和应用都步入一个新的阶段。为此，华章公司将加大引进教材的力度，在"华章教育"的总规划之下出版三个系列的计算机教材：除"计算机科学丛书"之外，对影印版的教材，则单独开辟出"经典原版书库"；同时，引进全美通行的教学辅导书"Schaum's Outlines"系列组成"全美经典学习指导系列"。为了保证这三套丛书的权威性，同时也为了更好地为学校和老师们服务，华章公司聘请了中国科学院、北京大学、清华大学、国防科技大学、复旦大学、上海交通大学，南京大学、浙江大学、中国科技大学、哈尔滨工业大学、西安交通大学、中国人民大学、北京航空航天大学、北京邮电大学、中山大学、解放军理工大学、郑州大学、湖北工学院、中国国家信息安全测评认证中心等国内重点大学和科研机构在计算机的各个领域的著名学者组成"专家指导委员会"，为我们提供选题意见和出版监督。
这三套丛书是响应教育部提出的使用外版教材的号召，为国内高校的计算机及相关专业的教学度身订造的。其中许多教材均已为M．I．T．，Stanford，U．C．Berkeley，C．M．U．等世界名牌大学所采用。不仅涵盖了程序设计、数据结构、操作系统、计算机体系结构、数据库、编译原理、软件工程、图形学、通信与网络、离散数学等国内大学计算机专业普遍开设的核心课程，而且各具特色--有的出自语言设计者之手、有的历经三十年而不衰、有的已被全世界的几百所高校采用。在这些圆熟通博的名师大作的指引之下，读者必将在计算机科学的宫殿中由登堂而入室。
权威的作者、经典的教材、一流的译者、严格的审校、精细的编辑，这些因素使我们的图书有了质量的保证，但我们的目标是尽善尽美，而反馈的意见正是我们达到这一终极目标的重要帮助。教材的出版只是我们的后续服务的起点。华章公司欢迎老师和读者对我们的工作提出建议或给予指正，我们的联系方法如下：
电子邮件：hzedu@hzbook．com
联系电话：(010)68995264
联系地址：北京市西城区百万庄南街1号
邮政编码：100037
近年，在全球信息化大潮的推动下，我国的计算机产业发展迅猛，对专业人才的需求日益迫切。这对计算机教育界和出版界都既是机遇，也是挑战；而专业教材的建设在教育战略上显得举足轻重。在我国信息技术发展时间较短、从业人员较少的现状下，美国等发达国家在其计算机科学发展的几十年间积淀的经典教材仍有许多值得借鉴之处。因此，引进一批国外优秀计算机教材将对我国计算机教育事业的发展起积极的推动作用，也是与世界接轨、建设真正的世界一流大学的必由之路。
机械工业出版社华章图文信息有限公司较早意识到"出版要为教育服务"。自1998年开始，华章公司就将工作重点放在了遴选、移译国外优秀教材上。经过几年的不懈努力，我们与Prentice Hall，Addison-Wesley，McGraw-Hill，MorganKaufmann等世界著名出版公司建立了良好的合作关系，从它们现有的数百种教材中甄选出Tanenbaum，Stroustrup，Kernighan，JimGray等大师名家的一批经典作品，以"计算机科学丛书"为总称出版，供读者学习、研究及庋藏。大理石纹理的封面，也正体现了这套丛书的品位和格调。
"计算机科学丛书"的出版工作得到了国内外学者的鼎力襄助，国内的专家不仅提供了中肯的选题指导，还不辞劳苦地担任了翻译和审校的工作；而原书的作者也相当关注其作品在中国的传播，有的还专诚为其书的中译本作序。迄今，"计算机科学丛书"已经出版了近百个品种，这些书籍在读者中树立了良好的口碑，并被许多高校采用为正式教材和参考书籍，为进一步推广与发展打下了坚实的基础。
随着学科建设的初步完善和教材改革的逐渐深化，教育界对国外计算机教材的需求和应用都步入一个新的阶段。为此，华章公司将加大引进教材的力度，在"华章教育"的总规划之下出版三个系列的计算机教材：除"计算机科学丛书"之外，对影印版的教材，则单独开辟出"经典原版书库"；同时，引进全美通行的教学辅导书"Schaum's Outlines"系列组成"全美经典学习指导系列"。为了保证这三套丛书的权威性，同时也为了更好地为学校和老师们服务，华章公司聘请了中国科学院、北京大学、清华大学、国防科技大学、复旦大学、上海交通大学，南京大学、浙江大学、中国科技大学、哈尔滨工业大学、西安交通大学、中国人民大学、北京航空航天大学、北京邮电大学、中山大学、解放军理工大学、郑州大学、湖北工学院、中国国家信息安全测评认证中心等国内重点大学和科研机构在计算机的各个领域的著名学者组成"专家指导委员会"，为我们提供选题意见和出版监督。
这三套丛书是响应教育部提出的使用外版教材的号召，为国内高校的计算机及相关专业的教学度身订造的。其中许多教材均已为M．I．T．，Stanford，U．C．Berkeley，C．M．U．等世界名牌大学所采用。不仅涵盖了程序设计、数据结构、操作系统、计算机体系结构、数据库、编译原理、软件工程、图形学、通信与网络、离散数学等国内大学计算机专业普遍开设的核心课程，而且各具特色--有的出自语言设计者之手、有的历经三十年而不衰、有的已被全世界的几百所高校采用。在这些圆熟通博的名师大作的指引之下，读者必将在计算机科学的宫殿中由登堂而入室。
权威的作者、经典的教材、一流的译者、严格的审校、精细的编辑，这些因素使我们的图书有了质量的保证，但我们的目标是尽善尽美，而反馈的意见正是我们达到这一终极目标的重要帮助。教材的出版只是我们的后续服务的起点。华章公司欢迎老师和读者对我们的工作提出建议或给予指正，我们的联系方法如下：
电子邮件：hzedu@hzbook．com
联系电话：(010)68995264
联系地址：北京市西城区百万庄南街1号
邮政编码：100037
前言
Our motivation for (re)writing this book One of the leitmotifs of writing the first edition of our book was the observation that most logics used in the design, specification and verification of computer systems fundamentally deal with a satisfaction relation where M is some sort of situation or model of a system, and qb is a specification, a formula of that logic, expressing what should be true in situation M. At the heart of this set-up is that one can often specify and implement algorithms for computing We developed this theme for propositional, first-order, temporal, modal, and program logics. Based on the encouraging feedback received from five continents we are pleased to hereby present the second edition of this text which means to preserve and improve on the original intent of the first edition.
What's new and what's gone
Chapter I now discusses the design, correctness, and complexity of a SAT solver (a marking algorithm similar to Stalmarck's method [SS90]) for full propositional logic.
Chapter 2 now contains basic results from model theory (Compactness Theorem and LSwenheim-Skolem Theorem); a section on the transitive closure and the expressiveness of existential and universal second-order logic; and a section on the use of the object modelling language Alloy and its analyser for specifying and exploring under-specified first-order logic models with respect to properties written in first-order logic with transitive closure. The Alloy language is executable which makes such exploration interactive and formal.
Chapter 3 has been completely restructured. It now begins with a discussion of linear-time temporal logic; features the open-source NuSMV modelchecking tool throughout; and includes a discussion on planning problems, more material on the expressiveness of temporal logics, and new modelling examples.
Chapter 4 contains more material on total correctness proofs and a new section on the programming-by-contract paradigm of verifying program correctness.
Chapters 5 and 6 have also been revised, with many small alterations and corrections.
The interdependence of chapters and prerequisites The book requires that students know the basics of elementary arithmetic and naive set theoretic concepts and notation. The core material of Chapter 1 (everything except Sections 1.4.3 to 1.6.2) is essential for all of the chapters that follow. Other than that, only Chapter 6 depends on Chapter 3 and a basic understanding of the static scoping rules covered in Chapter 2 although one may easily cover Sections 6.1 and 6.2 without having done Chapter 3 at all. Roughly, the interdependence diagram of chapters is This book is supported by a Web page, which contains a list of errata; text files for all the program code; ancillary technical material and links; all the figures; an interactive tutor based on multiple-choice questions; and details of how instructors can obtain the solutions to exercises in this book which are marked with a *. The URL for the book's page is www. cs.bham.ac.uk/research/lics/. See also www. cambridge.org/ 052154310x
What's new and what's gone
Chapter I now discusses the design, correctness, and complexity of a SAT solver (a marking algorithm similar to Stalmarck's method [SS90]) for full propositional logic.
Chapter 2 now contains basic results from model theory (Compactness Theorem and LSwenheim-Skolem Theorem); a section on the transitive closure and the expressiveness of existential and universal second-order logic; and a section on the use of the object modelling language Alloy and its analyser for specifying and exploring under-specified first-order logic models with respect to properties written in first-order logic with transitive closure. The Alloy language is executable which makes such exploration interactive and formal.
Chapter 3 has been completely restructured. It now begins with a discussion of linear-time temporal logic; features the open-source NuSMV modelchecking tool throughout; and includes a discussion on planning problems, more material on the expressiveness of temporal logics, and new modelling examples.
Chapter 4 contains more material on total correctness proofs and a new section on the programming-by-contract paradigm of verifying program correctness.
Chapters 5 and 6 have also been revised, with many small alterations and corrections.
The interdependence of chapters and prerequisites The book requires that students know the basics of elementary arithmetic and naive set theoretic concepts and notation. The core material of Chapter 1 (everything except Sections 1.4.3 to 1.6.2) is essential for all of the chapters that follow. Other than that, only Chapter 6 depends on Chapter 3 and a basic understanding of the static scoping rules covered in Chapter 2 although one may easily cover Sections 6.1 and 6.2 without having done Chapter 3 at all. Roughly, the interdependence diagram of chapters is This book is supported by a Web page, which contains a list of errata; text files for all the program code; ancillary technical material and links; all the figures; an interactive tutor based on multiple-choice questions; and details of how instructors can obtain the solutions to exercises in this book which are marked with a *. The URL for the book's page is www. cs.bham.ac.uk/research/lics/. See also www. cambridge.org/ 052154310x
序言
by
Edmund M. Clarke
FORE Systems Professor of Computer Science
Carnegie Mellon University
Pittsburgh, PA
Formal methods have finally come of age! Specification languages, theorem provers, and model checkers are beginning to be used routinely in industry. Mathematical logic is basic to all of these techniques. Until now textbooks on logic for computer scientists have not kept pace with the development of tools for hardware and software specification and verification. For example, in spite of the success of model checking in verifying sequential circuit designs and communication protocols, until now I did not know of a single text, suitable for undergraduate and beginning graduate students, that attempts to explain how this technique works. As a result, this material is rarely taught to computer scientists and electrical engineers who will need to use it as part of their jobs in the near future. Instead, engineers avoid using formal methods in situations where the methods would be of genuine benefit or complain that the concepts and notation used by the tools are complicated and unnatural. This is unfortunate since the underlying mathematics is generally quite simple, certainly no more difficult than the concepts from mathematical analysis that every calculus student is expected to learn.
Logic in Computer Science by Huth and Ryan is an exceptional book. I was amazed when I looked through it for the first time. In addition to propositional and predicate logic, it has a particularly thorough treatment of temporal logic and model checking. In fact, the book is quite remarkable in how much of this material it is able to cover: linear and branching time temporal logic, explicit state model checking, fairness, the basic fixpoint theorems for computation tree logic (CTL), even binary decision diagrams and symbolic model checking. Moreover, this material is presented at a level that is accessible to undergraduate and beginning graduate students. Numerous problems and examples are provided to help students master the material in the book. Since both Huth and Ryan are active researchers in logics of programs and program verification, they write with considerable authority.
In summary, the material in this book is up-to-date, practical, and elegantly presented. The book is a wonderful example of what a modern text on logic for computer science should be like. I recommend it to the reader with greatest enthusiasm and predict that the book will be an enormous success.
(This foreword is re-printed in the second edition with its author's permis-sion.)
Edmund M. Clarke
FORE Systems Professor of Computer Science
Carnegie Mellon University
Pittsburgh, PA
Formal methods have finally come of age! Specification languages, theorem provers, and model checkers are beginning to be used routinely in industry. Mathematical logic is basic to all of these techniques. Until now textbooks on logic for computer scientists have not kept pace with the development of tools for hardware and software specification and verification. For example, in spite of the success of model checking in verifying sequential circuit designs and communication protocols, until now I did not know of a single text, suitable for undergraduate and beginning graduate students, that attempts to explain how this technique works. As a result, this material is rarely taught to computer scientists and electrical engineers who will need to use it as part of their jobs in the near future. Instead, engineers avoid using formal methods in situations where the methods would be of genuine benefit or complain that the concepts and notation used by the tools are complicated and unnatural. This is unfortunate since the underlying mathematics is generally quite simple, certainly no more difficult than the concepts from mathematical analysis that every calculus student is expected to learn.
Logic in Computer Science by Huth and Ryan is an exceptional book. I was amazed when I looked through it for the first time. In addition to propositional and predicate logic, it has a particularly thorough treatment of temporal logic and model checking. In fact, the book is quite remarkable in how much of this material it is able to cover: linear and branching time temporal logic, explicit state model checking, fairness, the basic fixpoint theorems for computation tree logic (CTL), even binary decision diagrams and symbolic model checking. Moreover, this material is presented at a level that is accessible to undergraduate and beginning graduate students. Numerous problems and examples are provided to help students master the material in the book. Since both Huth and Ryan are active researchers in logics of programs and program verification, they write with considerable authority.
In summary, the material in this book is up-to-date, practical, and elegantly presented. The book is a wonderful example of what a modern text on logic for computer science should be like. I recommend it to the reader with greatest enthusiasm and predict that the book will be an enormous success.
(This foreword is re-printed in the second edition with its author's permis-sion.)
