Logic in Computer Science

OMeGa 2013-11-21 0

入门还可以，就是作者实在废话太多了

刷子 2013-02-05 0

非常不错的一本数理逻辑书，作为入门有些困难，但看下去就会好很多了。

Arwennnnnnn 2015-02-04 1

_(:з」∠)_

豌豆黄 2016-09-09 0

脉络清晰，和 programming 联系的部分详实具体，这一部分超过许多书籍，logic in cs 名副其实

可可 2008-03-22 0

Logic

[已注销] 2013-02-15 0

不合用

Larenopfer 2014-01-22 0

啰嗦但不错，不用考试的课就是舒服啊

Arwennnnnnn 2015-02-04 1

_(:з」∠)_

OMeGa 2013-11-21 0

入门还可以，就是作者实在废话太多了

刷子 2013-02-05 0

非常不错的一本数理逻辑书，作为入门有些困难，但看下去就会好很多了。

豌豆黄 2016-09-09 0

脉络清晰，和 programming 联系的部分详实具体，这一部分超过许多书籍，logic in cs 名副其实

可可 2008-03-22 0

Logic

[已注销] 2013-02-15 0

不合用

Larenopfer 2014-01-22 0

啰嗦但不错，不用考试的课就是舒服啊

我想说两句

Review from reviews.com

karenyskcau 2007-05-07 1赞

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 ... )

无可奈何的Delay

纳兰经若 2009-03-11 17赞

    某日在CU上与人瞎掰，其间谈到SICP序言太过深奥，于是有人抱怨道：我从来不看序，都是些吹捧之辞，毫无价值云云。要放到平时，我会十分赞同这个观点，如果你觉得有失偏颇，那在豆瓣上随便搜一堆书找出序言来看看是否大部分异曲同工、马屁之声不绝于耳。可问题这次谈及SICP，我便有些隐隐心痛————这可是Perlis写的序，再说，也没有大师给小弟拍马的道理。Perlis在这篇序言中引用了很多当年他自己的名篇《编程警言》的句子，看上去似乎数学味道很浓很艰深，实则为一篇充满诙谐幽默的随笔。要不怎么说人家是大师，光知道嘣俩牛B词汇出来吓唬人怎么行。回想某些国内大师的著作，翻开我就晕了，几乎是全面颠覆我以前的理解，每每及此，我便感慨：这世界真是变化快，咱国内的计算机水平都超越老外了，都全面颠覆计算理论了。然后不由得为自己的不学无术和落后感到脸红，估摸这自己这水水，还是继续看SICP之类的幼儿教科书比较实在，国内大师之巨著就暂时不敢奢望了。
    这本LCS吸引我的同样是序言，当然由于我了解信息的局限性，直到08年我才真正认识到这篇序言的价值，因为序言的作者E.Clark在08年因Model Checking而获图灵奖。而本书，恰是Model Checking的理论基础。再看译本出版时间为07年7月，我便深刻感受到本书译者对于计算科学发展方向的敏感性。要知道本书出版近8个月后，Model Checking才由于图灵奖而被众人熟知。所以本书绝不是什么应景之作，反而可说是极具洞察的一本书。
    不过么～Clark相比Perlis来，或许在学术上青出于蓝，要说整体素质，离伯大师还差得远。光对比序言水平就能看出来，Perlis可说是综合数学、艺术、文学的大师，而Clark就是一典型的科学家。恩～这样的一种对比当然从实际意义上来说毫无价值，纯粹是个人感情抒发，对本书有兴趣的人千万不要被这个对比打击到热情。
    本书另一处令人惊奇的地方，是二位作者来自于英国学校，这或许让不少关注计算科学书籍的人感到略微意外，毕竟在很多人心目中，MIT博克利斯坦福CM等等美国院校才应该与牛书挂钩才是。哎～要是图灵在天得知世人皆如此仰视米国而忽视其祖国，不知其做何感受。
    对于本书的价值，应该说懂得的人不需要听解释，不懂的人估计解释了也没用。或许可以用这么一个简单的例子来说明本书价值：可能有的朋友立志于开发中国的Quartus、ModelSim什么的，那你们有福了，本书可以带你们跨入理论门槛。当然你可能会有这样的担心，Qartus之流都基于特定的平台，即便我们研究了，能写软件了，以中国目前的硬件发展水平，怕也是望梅止渴。你能这么想，是很好的，至少说明你不是埋头撞墙的书呆子。不过正像我前面说的，这个世界发展太快了，现在OpenSparc这么火爆，我个人认为，有志向的人还是不要担忧自己很牛B了，周围却没有牛B的人来响应，而更应该担心别人牛B起来了，自己却没本事响应别人。如果你觉得自己很牛B了，但身边的人很磋，那说明你不够牛B。一个真正牛B的人，不可能身边围绕着一群磋人。
    恩～在这里还是要悄悄说一句，本书的价值可不仅仅在于能开发个Quartus之类除了能赚钱外一无是处的东东，更为关键的价值在于系统验证。这才是一统天下的不二法宝，因为你的验证水平很高的情况下，就可以制定标准，有了标准等同于列土封王。当然，这是学术上的了，不大适合个人发展，我觉得对于普通人来说能写个Quartus当个首富什么的也就算功成名就了。
    就本书内容而言，主要就是两部分，前两章讲归约，后面的讲验证。本质上来说，归约是为了简化问题以方便验证，验证是为了保证系统能如预定般工作。整套形式化验证理论不外乎就是这么简单一句话，不过越简单的描述才越发令人毛骨悚然。总之，在这么一个简单描述的背后，隐含的是非常艰难的研究工作。本书我只打4颗星，对于大部分人来说，知道这本书的背景和大体内容，就算不错了。真正愿意研究下去的人，恐怕也不屑于此书。

无可奈何的Delay

纳兰经若 2009-03-11 17

    某日在CU上与人瞎掰，其间谈到SICP序言太过深奥，于是有人抱怨道：我从来不看序，都是些吹捧之辞，毫无价值云云。要放到平时，我会十分赞同这个观点，如果你觉得有失偏颇，那在豆瓣上随便搜一堆书找出序言来看看是否大部分异曲同工、马屁之声不绝于耳。可问题这次谈及SICP，我便有些隐隐心痛————这可是Perlis写的序，再说，也没有大师给小弟拍马的道理。Perlis在这篇序言中引用了很多当年他自己的名篇《编程警言》的句子，看上去似乎数学味道很浓很艰深，实则为一篇充满诙谐幽默的随笔。要不怎么说人家是大师，光知道嘣俩牛B词汇出来吓唬人怎么行。回想某些国内大师的著作，翻开我就晕了，几乎是全面颠覆我以前的理解，每每及此，我便感慨：这世界真是变化快，咱国内的计算机水平都超越老外了，都全面颠覆计算理论了。然后不由得为自己的不学无术和落后感到脸红，估摸这自己这水水，还是继续看SICP之类的幼儿教科书比较实在，国内大师之巨著就暂时不敢奢望了。
    这本LCS吸引我的同样是序言，当然由于我了解信息的局限性，直到08年我才真正认识到这篇序言的价值，因为序言的作者E.Clark在08年因Model Checking而获图灵奖。而本书，恰是Model Checking的理论基础。再看译本出版时间为07年7月，我便深刻感受到本书译者对于计算科学发展方向的敏感性。要知道本书出版近8个月后，Model Checking才由于图灵奖而被众人熟知。所以本书绝不是什么应景之作，反而可说是极具洞察的一本书。
    不过么～Clark相比Perlis来，或许在学术上青出于蓝，要说整体素质，离伯大师还差得远。光对比序言水平就能看出来，Perlis可说是综合数学、艺术、文学的大师，而Clark就是一典型的科学家。恩～这样的一种对比当然从实际意义上来说毫无价值，纯粹是个人感情抒发，对本书有兴趣的人千万不要被这个对比打击到热情。
    本书另一处令人惊奇的地方，是二位作者来自于英国学校，这或许让不少关注计算科学书籍的人感到略微意外，毕竟在很多人心目中，MIT博克利斯坦福CM等等美国院校才应该与牛书挂钩才是。哎～要是图灵在天得知世人皆如此仰视米国而忽视其祖国，不知其做何感受。
    对于本书的价值，应该说懂得的人不需要听解释，不懂的人估计解释了也没用。或许可以用这么一个简单的例子来说明本书价值：可能有的朋友立志于开发中国的Quartus、ModelSim什么的，那你们有福了，本书可以带你们跨入理论门槛。当然你可能会有这样的担心，Qartus之流都基于特定的平台，即便我们研究了，能写软件了，以中国目前的硬件发展水平，怕也是望梅止渴。你能这么想，是很好的，至少说明你不是埋头撞墙的书呆子。不过正像我前面说的，这个世界发展太快了，现在OpenSparc这么火爆，我个人认为，有志向的人还是不要担忧自己很牛B了，周围却没有牛B的人来响应，而更应该担心别人牛B起来了，自己却没本事响应别人。如果你觉得自己很牛B了，但身边的人很磋，那说明你不够牛B。一个真正牛B的人，不可能身边围绕着一群磋人。
    恩～在这里还是要悄悄说一句，本书的价值可不仅仅在于能开发个Quartus之类除了能赚钱外一无是处的东东，更为关键的价值在于系统验证。这才是一统天下的不二法宝，因为你的验证水平很高的情况下，就可以制定标准，有了标准等同于列土封王。当然，这是学术上的了，不大适合个人发展，我觉得对于普通人来说能写个Quartus当个首富什么的也就算功成名就了。
    就本书内容而言，主要就是两部分，前两章讲归约，后面的讲验证。本质上来说，归约是为了简化问题以方便验证，验证是为了保证系统能如预定般工作。整套形式化验证理论不外乎就是这么简单一句话，不过越简单的描述才越发令人毛骨悚然。总之，在这么一个简单描述的背后，隐含的是非常艰难的研究工作。本书我只打4颗星，对于大部分人来说，知道这本书的背景和大体内容，就算不错了。真正愿意研究下去的人，恐怕也不屑于此书。

Review from reviews.com

karenyskcau 2007-05-07 1

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 ... )

我要写长评

想读在读读过

标签(多个标签以“，”分开):

保存

Logic in Computer Science

推荐文章

猜你喜欢

附近的人在看

推荐阅读

拓展阅读