面向計算機(jī)科學(xué)的數(shù)理邏輯系統(tǒng)建模與推理

用戶評論 (總計11條)

•   很好，國外經(jīng)典，看了2遍了
•   書很好，經(jīng)典有深度，非常好。
•   十分經(jīng)典
•   書很好，很不錯，包裝也很好，推薦。
•   有時間要好好看一下！
•   就是這本書的紙張質(zhì)量不敢恭維
•   還好，值得一讀！
•   這本書看了前面的，后面還沒看完，直接看TLA這本書應(yīng)該更快上手寫代碼
•   這本書寫的滿清楚，我特別希望第3章的內(nèi)容。
•   計算機(jī)理論的好書
•   　　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 ... )
  　　
  　　

相關(guān)圖書

• 中國互聯(lián)網(wǎng)發(fā)展報告
• 計算機(jī)系統(tǒng)設(shè)計與結(jié)構(gòu)
• Web應(yīng)用測試
• Verilog HDL程序設(shè)計與應(yīng)用
• 新編Photoshop CS中文版入門與提高
• 網(wǎng)絡(luò)管理員考點精講與試題精解
• C語言實例解析精粹
• 孔子大傳
• 自白錄
• 李漁傳
• 圣潔的狂僧（上中下卷）
• 朱可夫元帥戰(zhàn)爭回憶錄
• 凱撒大帝（全二冊）
• 前廳疑難案例解析
• 機(jī)器貓 哆啦A夢29
• 孫齊齊七十二變（第一輯）
• 超長篇機(jī)器貓哆啦A夢3
• 官場現(xiàn)形記（上、下）
• 龍族戰(zhàn)神
• 毛澤東思想基本著作選讀
• 文字處理(教師用書) (平裝)
• 機(jī)器貓 哆啦A夢44
• 光棍趣事
• 零點陽光
• 我不另類