面向计算机科学的数理逻辑系统建模与推理

出版时间：2005-4  出版社：机械工业  作者：胡思  页数：427  
Tag标签：无  

内容概要

数理逻辑是计算机科学的基础之一，在模型与系统的规约与验证等方面有着广泛的应用。随着当今软硬件产品日趋复杂，数理逻辑已经成为越来越多设计开发人员的日常工具。    本书适合作为高等院校计算机及相关专业的数理逻辑/形式化方法课程教材，涵盖了命题逻辑，谓词逻辑、模态逻辑与 Agent、二元决策图、模型检查和程序验证等内容。与传统数理逻辑教科书相比，它的主要特色就是紧紧围绕软硬件规约和验证这一主题，反映了计算机科学中数理逻辑的新发展和实际需要。第2版新增了可满足性算法，紧致性理论和Lowenhenm-Skolem定理，并介绍了Alloy语言和Nusmv工具。    本书自出版以来受到广泛好评，已经被包括美国普林斯顿大学、卡内基-梅隆大学、英国剑桥大学、德国汉堡大学、加拿大多伦多大学、荷兰 Vrije大学，印度理工学院在内的多个国家几十所高校采纳为教材。

作者简介

Michael Huth，伦敦帝国学院计算机系高级讲师，研究方向包括模型检测与抽象，程序分析和模型检测中有序结构的应用等。

书籍目录

Foreword to the first editionPreface to the second editionAcdnowledgements1 Propositional logic  1.1 Declarative sentences  1.2 Natural deauction    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 rormal languae  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    1.5.3 Horn clauses and satisfiability  1.6 SAT solvers    1.6.1 A linear solver    1.6.2 A cubic solver  1.7 Exercises  1.8 Bibliographic notes2 Predicate logic3 Verification by model checking4 Program verification5 Modal logics and agents6 Binary decision diagramsBibliographyIndex

用户评论 (总计11条)

•   很好，国外经典，看了2遍了
•   书很好，经典有深度，非常好。
•   十分经典
•   书很好，很不错，包装也很好，推荐。
•   有时间要好好看一下！
•   就是这本书的纸张质量不敢恭维
•   还好，值得一读！
•   这本书看了前面的，后面还没看完，直接看TLA这本书应该更快上手写代码
•   这本书写的满清楚，我特别希望第3章的内容。
•   计算机理论的好书
•   　　The plethora of textbooks giving a computing viewpoint on logic is evidence that logic is central to the study of computer science, but is there room for yet another? If this text covered the familiar ground, the answer would probably be “no,” but Huth and Ryan have chosen to illustrate their text with up-to-date, relevant, and challenging case studies of how logic is being used in practice, rather than the more pedestrian and predictable examples given in many texts. In particular, they cover model checking--which is arguably the great success story of the application of logic in computing over the last decade--as well as modal logics for reasoning about belief and the more traditional application of logic to imperative program verification.
  　　
  　　The first two chapters cover propositional and predicate logic, with an emphasis on proof in a natural deduction system. The most difficult aspect of natural deduction systems is the way in which assumptions are introduced and discharged; the authors use a box notation to delimit the scope of assumptions. Natural deduction systems are the best for the construction of proofs by the learner, and while no notation can make the discharge of assumptions into a routine operation, the authors’ choice makes good sense for the beginner. These chapters, and indeed the whole book, are well supplied with exercises that range from the routine to the more challenging.
  　　
  　　The third chapter is where the book departs from the well-trodden path by introducing model checking for the temporal logic computation tree logic (CTL), a branching time logic whose model checking problem is tractable. The model checking problem is to ascertain whether a particular structure--a finite structure of “possible worlds,” or a transition system--satisfies (“is a model for”) a formula of CTL. Model checking is attractive for a number of reasons. It can be performed automatically, it can be implemented efficiently (see remarks on chapter 6 below), and when a structure fails to satisfy a formula, the algorithm can produce a counterexample in the form of a trace of the system that does not exhibit the required behavior. The authors first introduce CTL and illustrate its use in practical specification problems. They then present a naive model checking algorithm and discuss its implementation in the SMV system.
  　　
  　　Chapter 6 contains an excellent exposition of binary decision diagrams (BDDs), a novel representation of Boolean functions. Given an ordering on the variables of a function, a reduced, ordered BDD gives a canonical representation of the Boolean function; more traditional representations such as conjunctive and disjunctive normal forms fail to have this property. Having canonical representations of Boolean functions has a number of consequences: testing for satisfiability and validity becomes a matter of checking equality with trivially true or false BDDs, and equality between functions can be checked by checking the equality of BDDs, which in turn can be performed simply by checking equality of pointers. The authors show how BDD representations can be built for arbitrary functions, and then extend this to representations of models, transition systems, and state sets. Thus, the naive model checking algorithm can be replaced by a symbolic algorithm, and on this basis, models with state sets of the order of 10100 can be efficiently checked.
  　　
  　　Chapters 4 and 5 cover Hoare logics for imperative program verification and modal logics for multi-agent systems. Both chapters give a clear view of the application and contain a comprehensive collection of exercises.
  　　
  　　The authors write well and convey their enthusiasm for the subject and its application. The text can be used for a higher-level undergraduate module, or as material in an introductory graduate course. Its style also lends it to self-study; supplementary materials, such as solutions to some of the exercises, are available on the Web. In summary, I recommend it highly.
  　　Reviewer: Simon Thompson Review #: CR122851 (0002-0071)
  　　
  　　
  　　Specifying And Verifying And Reasoning About Programs (F.3.1 )
  　　
  　　
  　　Modal Logic (F.4.1 ... )