面向计算机科学的数理逻辑系统建模与推理 英文版·第2版PDF|Epub|txt|kindle电子书版本网盘下载

面向计算机科学的数理逻辑系统建模与推理 英文版·第2版PDF格式电子书版下载

注意：本站所有压缩包均有解压码： 点击下载压缩包解压工具

1 Propositionallogic1

1.1 Declarative sentences2

1.2 Natural deduction5

1.2.1 Rules for natural deduction6

Contents7

Foreword to the first edition page7

Preface to the second edition9

Acknowledgements11

1.2.2 Derived rules23

1.2.3 Natural deduction in summary26

1.2.4 Provable equivalence29

1.2.5 An aside:proof by contradiction29

1.3 Propositional logic as a formal language31

1.4 Semantics of propositional logic36

1.4.1 The meaning of logical connectives36

1.4.2 Mathematical induction40

1.4.3 Soundness of propositional logic45

1.4.4 Completeness of propositional logic49

1.5 Normal forms53

1.5.1 Semantic equivalence,satisfiability and validity54

1.5.2 Conjunctive normal forms and validity58

1.5.3 Horn clauses and satisfiability65

1.6 SAT solvers68

1.6.1 A linear solver69

1.6.2 A cubic solver72

1.7 Exercises78

1.8 Bibliographic notes91

2 Predicate logic93

2.1 The need for a richer language93

2.2 Predicate logic as a formal language98

2.2.1 Terms99

2.2.2 Formulas100

2.2.3 Free and bound variables102

2.2.4 Substitution104

2.3.1 Natural deduction rules107

2.3 Proof theory of predicate logic107

2.3.2 Quantifier equivalences117

2.4 Semantics of predicate logic122

2.4.1 Models123

2.4.2 Semantic entailment129

2.4.3 The semantics of equality130

2.5 Undecidability of predicate logic131

2.6 Expressiveness of predicate logic136

2.6.1 Existential second-order logic139

2.6.2 Universal second-order logic140

2.7 Micromodels of software141

2.7.1 State machines142

2.7.2 Alma-re-visited146

2.7.3 A software micromodel148

2.8 Exercises157

2.9 Bibliographic notes170

3.1 Motivation for verification172

3 Verification by model checking172

3.2 Linear-time temporal logic175

3.2.1 Syntax of LTL175

3.2.2 Semantics of LTL178

3.2.3 Practical patterns of specifications183

3.2.4 Important equivalences between LTL formulas184

3.2.5 Adequate sets of connectives for LTL186

3.3.1 Example:mutual exclusion187

3.3 Model checking:systems,tools,properties187

3.3.2 The NuSMV model checker191

3.3.3 Running NuSMV194

3.3.4 Mutual exclusion revisited195

3.3.5 The ferryman199

3.3.6 The alternating bit protocol203

3.4 Branching-time logic207

3.4.1 Syntax of CTL208

3.4.2 Semantics of CTL211

3.4.4 Important equivalences between CTL formulas215

3.4.3 Practical patterns of specifications215

3.4.5 Adequate sets of CTL connectives216

3.5 CTL*and the expressive powers of LTL and CTL217

3.5.1 Boolean combinations of temporal formulas in CTL220

3.5.2 Past operators in LTL221

3.6 Model-checking algorithms221

3.6.1 The CTL model-checking algorithm222

3.6.2 CTL model checking with fairness230

3.6.3 The LTL model-checking algorithm232

3.7 The fixed-point characterisation of CTL238

3.7.1 Monotone functions240

3.7.2 The correctness of SATEG242

3.7.3 The correctness of SATEU243

3.8 Exercises245

3.9 Bibliographic notes254

4 Program verification256

4.1 Why should we specify and verify code？257

4.2 A framework for software verification258

4.2.1 A core programming language259

4.2.2 Hoare triples262

4.2.3 Partial and total correctness265

4.2.4 Program variables and logical variables268

4.3 Proof calculus for partial correctness269

4.3.1 Proof rules269

4.3.2 Proof tableaux273

4.3.3 A case study:minimal-sum section287

4.4 Proof calculus for total correctness292

4.5 Programming by contract296

4.6 Exercises299

4.7 Bibliographic notes304

5 Modal logics and agents306

5.1 Modes of truth306

5.2 Basic modal logic307

5.2.1 Syntax307

5.2.2 Semantics308

5.3 Logic engineering316

5.3.1 The stock of valid formulas317

5.3.2 Important properties of the accessibility relation320

5.3.3 Correspondence theory322

5.3.4 Some modal logics326

5.4 Natural deduction328

5.5 Reasoning about knowledge in a multi-agent system331

5.5.1 Some examples332

5.5.2 The modallogic KT45n335

5.5.3 Natural deduction for KT45n339

5.5.4 Formalising the examples342

5.6 Exercises350

5.7 Bibliographic notes356

6 Binary decision diagrams358

6.1 Representing boolean functions358

6.1.1 Propositional formulas and truth tables359

6.1.2 Binary decision diagrams361

6.1.3 Ordered BDDs366

6.2.1 The algorithm reduce372

6.2 Algorithms for reduced OBDDs372

6.2.2 The algorithm apply373

6.2.3 The algorithm restrict377

6.2.4 The algorithm exists377

6.2.5 Assessment of OBDDs380

6.3 Symbolic model checking382

6.3.1 Representing subsets of the set of states383

6.3.2 Representing the transition relation385

6.3.3 Implementing the functions pre？ and pre？387

6.3.4 Synthesising OBDDs387

6.4 A relational mu-calculus390

6.4.1 Syntax and semantics390

6.4.2 Coding CTL models and specifications393

6.5 Exercises398

6.6 Bibliographic notes413

Bibliography414

Index418