科研帝上线啦!115万本专业的英文电子书全部免费下载!

科研帝

 找回密码
 立即注册

手机号码,快捷登录

金币不够用?来这充值VIP学者,无限量下载
查看: 116|回复: 1

Logic in computer science: modelling and reasoning about systems-[2nd ed]-[pdf]-[Michael Huth, Mark Ryan]

[复制链接]
  • TA的每日心情
    开心
    2018-10-7 11:51
  • 签到天数: 68 天

    [LV.6]常住居民II

    23

    主题

    101

    帖子

    217

    积分

    管理员

    Rank: 9Rank: 9Rank: 9

    金币
    1184
    关注领域
    物理学
    QQ
    发表于 2017-10-26 12:14:33 | 显示全部楼层 |阅读模式
    提示:本书回复后可见下载链接(点击链接后等待30秒内会自动启动下载),普通用户回复扣5金币,VIP用户免费下载。还不是VIP?点击这里加入VIP→


    免费下载30页预览文件

    书籍信息:
    标题: Logic in computer science: modelling and reasoning about systems
    语言: English
    格式: pdf
    大小: 2.0M
    页数: 443
    年份: 2004
    作者: Michael Huth, Mark Ryan
    版次: 2nd ed
    出版社: Cambridge University Press

    简介

    Recent years have seen the development of powerful tools for verifying hardware and software systems, as companies worldwide realise the need for improved means of validating their products. There is increasing demand for training in basic methods in formal reasoning so that students can gain proficiency in logic-based verification methods. The second edition of this successful textbook addresses both those requirements, by continuing to provide a clear introduction to formal reasoning which is both relevant to the needs of modern computer science and rigorous enough for practical application. Improvements to the first edition have been made throughout, with extra and expanded sections on SAT solvers, existential/universal second-order logic, micro-models, programming by contract and total correctness. The coverage of model-checking has been substantially updated. Further exercises have been added. Internet support for the book includes worked solutions for all exercises for teachers, and model solutions to some exercises for students.


    目录
    Cover......Page 1
    Half-title......Page 3
    Title......Page 5
    Copyright......Page 6
    Contents......Page 7
    Foreword to the first edition......Page 11
    What’s new and what’s gone......Page 13
    The interdependence of chapters and prerequisites......Page 14
    Added for second edition......Page 15
    1 Propositional logic......Page 17
    1.1 Declarative sentences......Page 18
    1.2 Natural deduction......Page 21
    1.2.1 Rules for natural deduction......Page 22
    1.2.2 Derived rules......Page 39
    1.2.3 Natural deduction in summary......Page 42
    1.2.5 An aside: proof by contradiction......Page 45
    1.3 Propositional logic as a formal language......Page 47
    1.4.1 The meaning of logical connectives......Page 52
    1.4.2 Mathematical induction......Page 56
    1.4.3 Soundness of propositional logic......Page 61
    1.4.4 Completeness of propositional logic......Page 65
    1.5 Normal forms......Page 69
    1.5.1 Semantic equivalence, satisfiability and validity......Page 70
    1.5.2 Conjunctive normal forms and validity......Page 74
    1.5.3 Horn clauses and satisfiability......Page 81
    1.6 SAT solvers......Page 84
    1.6.1 A linear solver......Page 85
    1.6.2 A cubic solver......Page 88
    1.7 Exercises......Page 94
    1.8 Bibliographic notes......Page 107
    2.1 The need for a richer language......Page 109
    2.2 Predicate logic as a formal language......Page 114
    2.2.1 Terms......Page 115
    2.2.2 Formulas......Page 116
    2.2.3 Free and bound variables......Page 118
    2.2.4 Substitution......Page 120
    2.3.1 Natural deduction rules......Page 123
    2.3.2 Quantifier equivalences......Page 133
    2.4 Semantics of predicate logic......Page 138
    2.4.1 Models......Page 139
    2.4.2 Semantic entailment......Page 145
    2.4.3 The semantics of equality......Page 146
    2.5 Undecidability of predicate logic......Page 147
    2.6 Expressiveness of predicate logic......Page 152
    2.6.1 Existential second-order logic......Page 155
    2.6.2 Universal second-order logic......Page 156
    2.7 Micromodels of software......Page 157
    2.7.1 State machines......Page 158
    2.7.2 Alma – re-visited......Page 162
    2.7.3 A software micromodel......Page 164
    2.8 Exercises......Page 173
    2.9 Bibliographic notes......Page 186
    3.1 Motivation for verification......Page 188
    3.2.1 Syntax of LTL......Page 191
    3.2.2 Semantics of LTL......Page 194
    3.2.3 Practical patterns of specifications......Page 199
    3.2.4 Important equivalences between LTL formulas......Page 200
    3.2.5 Adequate sets of connectives for LTL......Page 202
    3.3.1 Example: mutual exclusion......Page 203
    3.3.2 The NuSMV model checker......Page 207
    3.3.3 Running NuSMV......Page 210
    3.3.4 Mutual exclusion revisited......Page 211
    3.3.5 The ferryman......Page 215
    3.3.6 The alternating bit protocol......Page 219
    3.4 Branching-time logic......Page 223
    3.4.1 Syntax of CTL......Page 224
    3.4.2 Semantics of computation tree logic......Page 227
    3.4.4 Important equivalences between CTL formulas......Page 231
    3.4.5 Adequate sets of CTL connectives......Page 232
    3.5 CTL and the expressive powers of LTL and CTL......Page 233
    3.5.1 Boolean combinations of temporal formulas in CTL......Page 236
    3.6 Model-checking algorithms......Page 237
    3.6.1 The CTL model-checking algorithm......Page 238
    3.6.2 CTL model checking with fairness......Page 246
    3.6.3 The LTL model-checking algorithm......Page 248
    3.7 The fixed-point characterisation of CTL......Page 254
    3.7.1 Monotone functions......Page 256
    3.7.2 The correctness of SATEG......Page 258
    3.7.3 The correctness of SATEU......Page 259
    3.8 Exercises......Page 261
    3.9 Bibliographic notes......Page 270
    4 Program verification......Page 272
    4.1 Why should we specify and verify code?......Page 273
    4.2 A framework for software verification......Page 274
    4.2.1 A core programming language......Page 275
    4.2.2 Hoare triples......Page 278
    4.2.3 Partial and total correctness......Page 281
    4.2.4 Program variables and logical variables......Page 284
    4.3.1 Proof rules......Page 285
    4.3.2 Proof tableaux......Page 289
    4.3.3 A case study: minimal-sum section......Page 303
    4.4 Proof calculus for total correctness......Page 308
    4.5 Programming by contract......Page 312
    4.6 Exercises......Page 315
    4.7 Bibliographic notes......Page 320
    5.1 Modes of truth......Page 322
    5.2.1 Syntax......Page 323
    5.2.2 Semantics......Page 324
    Equivalences between modal formulas......Page 329
    Valid formulas......Page 330
    5.3 Logic engineering......Page 332
    5.3.1 The stock of valid formulas......Page 333
    5.3.2 Important properties of the accessibility relation......Page 336
    5.3.3 Correspondence theory......Page 338
    5.3.4 Some modal logics......Page 342
    5.4 Natural deduction......Page 344
    5.5 Reasoning about knowledge in a multi-agent system......Page 347
    5.5.1 Some examples......Page 348
    5.5.2 The modal logic KT45n......Page 351
    5.5.3 Natural deduction for KT45n......Page 355
    5.5.4 Formalising the examples......Page 358
    5.6 Exercises......Page 366
    5.7 Bibliographic notes......Page 372
    6.1 Representing boolean functions......Page 374
    6.1.1 Propositional formulas and truth tables......Page 375
    6.1.2 Binary decision diagrams......Page 377
    6.1.3 Ordered BDDs......Page 382
    6.2.1 The algorithm reduce......Page 388
    6.2.2 The algorithm apply......Page 389
    6.2.4 The algorithm exists......Page 393
    6.2.5 Assessment of OBDDs......Page 396
    6.3 Symbolic model checking......Page 398
    6.3.1 Representing subsets of the set of states......Page 399
    6.3.2 Representing the transition relation......Page 401
    6.3.4 Synthesising OBDDs......Page 403
    6.4.1 Syntax and semantics......Page 406
    6.5 Exercises......Page 414
    6.6 Bibliographic notes......Page 429
    Bibliography......Page 430
    Index......Page 434

    电子书下载地址回复可见:
    游客,如果您要查看本帖隐藏内容请回复

    每天进步一点点
    回复

    使用道具 举报

    该用户从未签到

    0

    主题

    12

    帖子

    12

    积分

    小学生

    Rank: 1

    金币
    33
    发表于 2018-5-19 13:34:37 | 显示全部楼层
    Recent years have seen the development of powerful tools for verifying
    回复

    使用道具 举报

    您需要登录后才可以回帖 登录 | 立即注册

    本版积分规则

    关闭

    站长推荐上一条 /1 下一条

    QQ|Archiver|手机版|小黑屋|科研帝   

    GMT+8, 2018-10-21 02:23 , Processed in 0.060712 second(s), 30 queries .

    Powered by Discuz! X3.4

    © 2001-2017 Comsenz Inc.

    快速回复 返回顶部 返回列表