面向计算机科学的数理逻辑系统建模与推理 英文版·第2版PDF电子书下载
- 电子书积分:14 积分如何计算积分?
- 作 者:(英)胡思(Huth,M.)伦敦帝国学院(MICHAELHuth)著
- 出 版 社:北京:机械工业出版社
- 出版年份:2005
- ISBN:7111160533
- 页数:427 页
1 Propositionallogic 1
1.1 Declarative sentences 2
1.2 Natural deduction 5
1.2.1 Rules for natural deduction 6
Contents 7
Foreword to the first edition page 7
Preface to the second edition 9
Acknowledgements 11
1.2.2 Derived rules 23
1.2.3 Natural deduction in summary 26
1.2.4 Provable equivalence 29
1.2.5 An aside:proof by contradiction 29
1.3 Propositional logic as a formal language 31
1.4 Semantics of propositional logic 36
1.4.1 The meaning of logical connectives 36
1.4.2 Mathematical induction 40
1.4.3 Soundness of propositional logic 45
1.4.4 Completeness of propositional logic 49
1.5 Normal forms 53
1.5.1 Semantic equivalence,satisfiability and validity 54
1.5.2 Conjunctive normal forms and validity 58
1.5.3 Horn clauses and satisfiability 65
1.6 SAT solvers 68
1.6.1 A linear solver 69
1.6.2 A cubic solver 72
1.7 Exercises 78
1.8 Bibliographic notes 91
2 Predicate logic 93
2.1 The need for a richer language 93
2.2 Predicate logic as a formal language 98
2.2.1 Terms 99
2.2.2 Formulas 100
2.2.3 Free and bound variables 102
2.2.4 Substitution 104
2.3.1 Natural deduction rules 107
2.3 Proof theory of predicate logic 107
2.3.2 Quantifier equivalences 117
2.4 Semantics of predicate logic 122
2.4.1 Models 123
2.4.2 Semantic entailment 129
2.4.3 The semantics of equality 130
2.5 Undecidability of predicate logic 131
2.6 Expressiveness of predicate logic 136
2.6.1 Existential second-order logic 139
2.6.2 Universal second-order logic 140
2.7 Micromodels of software 141
2.7.1 State machines 142
2.7.2 Alma-re-visited 146
2.7.3 A software micromodel 148
2.8 Exercises 157
2.9 Bibliographic notes 170
3.1 Motivation for verification 172
3 Verification by model checking 172
3.2 Linear-time temporal logic 175
3.2.1 Syntax of LTL 175
3.2.2 Semantics of LTL 178
3.2.3 Practical patterns of specifications 183
3.2.4 Important equivalences between LTL formulas 184
3.2.5 Adequate sets of connectives for LTL 186
3.3.1 Example:mutual exclusion 187
3.3 Model checking:systems,tools,properties 187
3.3.2 The NuSMV model checker 191
3.3.3 Running NuSMV 194
3.3.4 Mutual exclusion revisited 195
3.3.5 The ferryman 199
3.3.6 The alternating bit protocol 203
3.4 Branching-time logic 207
3.4.1 Syntax of CTL 208
3.4.2 Semantics of CTL 211
3.4.4 Important equivalences between CTL formulas 215
3.4.3 Practical patterns of specifications 215
3.4.5 Adequate sets of CTL connectives 216
3.5 CTL*and the expressive powers of LTL and CTL 217
3.5.1 Boolean combinations of temporal formulas in CTL 220
3.5.2 Past operators in LTL 221
3.6 Model-checking algorithms 221
3.6.1 The CTL model-checking algorithm 222
3.6.2 CTL model checking with fairness 230
3.6.3 The LTL model-checking algorithm 232
3.7 The fixed-point characterisation of CTL 238
3.7.1 Monotone functions 240
3.7.2 The correctness of SATEG 242
3.7.3 The correctness of SATEU 243
3.8 Exercises 245
3.9 Bibliographic notes 254
4 Program verification 256
4.1 Why should we specify and verify code? 257
4.2 A framework for software verification 258
4.2.1 A core programming language 259
4.2.2 Hoare triples 262
4.2.3 Partial and total correctness 265
4.2.4 Program variables and logical variables 268
4.3 Proof calculus for partial correctness 269
4.3.1 Proof rules 269
4.3.2 Proof tableaux 273
4.3.3 A case study:minimal-sum section 287
4.4 Proof calculus for total correctness 292
4.5 Programming by contract 296
4.6 Exercises 299
4.7 Bibliographic notes 304
5 Modal logics and agents 306
5.1 Modes of truth 306
5.2 Basic modal logic 307
5.2.1 Syntax 307
5.2.2 Semantics 308
5.3 Logic engineering 316
5.3.1 The stock of valid formulas 317
5.3.2 Important properties of the accessibility relation 320
5.3.3 Correspondence theory 322
5.3.4 Some modal logics 326
5.4 Natural deduction 328
5.5 Reasoning about knowledge in a multi-agent system 331
5.5.1 Some examples 332
5.5.2 The modallogic KT45n 335
5.5.3 Natural deduction for KT45n 339
5.5.4 Formalising the examples 342
5.6 Exercises 350
5.7 Bibliographic notes 356
6 Binary decision diagrams 358
6.1 Representing boolean functions 358
6.1.1 Propositional formulas and truth tables 359
6.1.2 Binary decision diagrams 361
6.1.3 Ordered BDDs 366
6.2.1 The algorithm reduce 372
6.2 Algorithms for reduced OBDDs 372
6.2.2 The algorithm apply 373
6.2.3 The algorithm restrict 377
6.2.4 The algorithm exists 377
6.2.5 Assessment of OBDDs 380
6.3 Symbolic model checking 382
6.3.1 Representing subsets of the set of states 383
6.3.2 Representing the transition relation 385
6.3.3 Implementing the functions pre? and pre? 387
6.3.4 Synthesising OBDDs 387
6.4 A relational mu-calculus 390
6.4.1 Syntax and semantics 390
6.4.2 Coding CTL models and specifications 393
6.5 Exercises 398
6.6 Bibliographic notes 413
Bibliography 414
Index 418
- 《卓有成效的管理者 中英文双语版》(美)彼得·德鲁克许是祥译;那国毅审校 2019
- 《程序逻辑及C语言编程》卢卫中,杨丽芳主编 2019
- 《AutoCAD 2018自学视频教程 标准版 中文版》CAD/CAM/CAE技术联盟 2019
- 《跟孩子一起看图学英文》张紫颖著 2019
- 《AutoCAD机械设计实例精解 2019中文版》北京兆迪科技有限公司编著 2019
- 《庆祝新中国成立70周年当代中国发展的逻辑系列丛书 当代中国生态发展的逻辑》熊捷责编;包存宽 2020
- 《弗雷格逻辑主义研究》刘靖贤著 2019
- 《概率论与数理统计》傅丽芳 2018
- 《复分析 英文版》(中国)李娜,马立新 2019
- 《行测判断推理》李永新主编 2019
- 《社会学与人类生活 社会问题解析 第11版》(美)James M. Henslin(詹姆斯·M. 汉斯林) 2019
- 《古代巴比伦》(英)莱昂纳德·W.金著 2019
- 《BBC人体如何工作》(英)爱丽丝.罗伯茨 2019
- 《一个数学家的辩白》(英)哈代(G.H.Hardy)著;李文林,戴宗铎,高嵘译 2019
- 《莎士比亚全集 2》(英)莎士比亚著,朱生豪等译 2002
- 《莎士比亚戏剧精选集》(英)威廉·莎士比亚(William Shakespeare)著 2020
- 《莎士比亚 叙事诗·抒情诗·戏剧》(英)威廉·莎士比亚著 2019
- 《亚历山大继业者战争 上 将领与战役》(英)鲍勃·本尼特,(英)麦克·罗伯茨著;张晓媛译 2019
- 《孩子们的音乐之旅 1 宝宝睡觉 幼儿版》包菊英主编 2016
- 《超级参与者》王金强责编;赵磊译者;(澳)杰里米·海曼斯,(英)亨利·蒂姆斯 2020
- 《指向核心素养 北京十一学校名师教学设计 英语 七年级 上 配人教版》周志英总主编 2019
- 《北京生态环境保护》《北京环境保护丛书》编委会编著 2018
- 《高等教育双机械基础课程系列教材 高等学校教材 机械设计课程设计手册 第5版》吴宗泽,罗圣国,高志,李威 2018
- 《指向核心素养 北京十一学校名师教学设计 英语 九年级 上 配人教版》周志英总主编 2019
- 《高等院校旅游专业系列教材 旅游企业岗位培训系列教材 新编北京导游英语》杨昆,鄢莉,谭明华 2019
- 《中国十大出版家》王震,贺越明著 1991
- 《近代民营出版机构的英语函授教育 以“商务、中华、开明”函授学校为个案 1915年-1946年版》丁伟 2017
- 《新工业时代 世界级工业家张毓强和他的“新石头记”》秦朔 2019
- 《智能制造高技能人才培养规划丛书 ABB工业机器人虚拟仿真教程》(中国)工控帮教研组 2019
- 《AutoCAD机械设计实例精解 2019中文版》北京兆迪科技有限公司编著 2019