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

用戶評(píng)論 (總計(jì)11條)

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

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