Logic in Computer Science.pdf

发布时间：2022-06-08 发布人：admin 分类：说明书资料大小：2.14M 资料格式：pdf 举报版权申诉

u011168556-5633631-4744302543362692320.pdf-第1页.png

第1页 / 共443页

u011168556-5633631-4744302543362692320.pdf-第2页.png

第2页 / 共443页

u011168556-5633631-4744302543362692320.pdf-第3页.png

第3页 / 共443页

u011168556-5633631-4744302543362692320.pdf-第4页.png

第4页 / 共443页

u011168556-5633631-4744302543362692320.pdf-第5页.png

第5页 / 共443页

u011168556-5633631-4744302543362692320.pdf-第6页.png

第6页 / 共443页

u011168556-5633631-4744302543362692320.pdf-第7页.png

第7页 / 共443页

u011168556-5633631-4744302543362692320.pdf-第8页.png

第8页 / 共443页

Cover

Half-title

Title

Contents

Foreword to the first edition

Preface to the second edition

Our motivation for (re)writing this book

What’s new and what’s gone

The interdependence of chapters and prerequisites

Acknowledgements

Added for second edition

1 Propositional logic

1.1 Declarative sentences

1.2 Natural deduction

1.2.1 Rules for natural deduction

1.2.2 Derived rules

1.2.3 Natural deduction in summary

1.2.4 Provable equivalence

1.2.5 An aside: proof by contradiction

1.3 Propositional logic as a formal language

1.4 Semantics of propositional logic

1.4.1 The meaning of logical connectives

1.4.2 Mathematical induction

1.4.3 Soundness of propositional logic

1.4.4 Completeness of propositional logic

1.5 Normal forms

1.5.1 Semantic equivalence, satisfiability and validity

1.5.2 Conjunctive normal forms and validity

1.5.3 Horn clauses and satisfiability

1.6 SAT solvers

1.6.1 A linear solver

1.6.2 A cubic solver

1.7 Exercises

1.8 Bibliographic notes

2 Predicate logic

2.1 The need for a richer language

2.2 Predicate logic as a formal language

2.2.1 Terms

2.2.2 Formulas

2.2.3 Free and bound variables

2.2.4 Substitution

2.3 Proof theory of predicate logic

2.3.1 Natural deduction rules

2.3.2 Quantifier equivalences

2.4 Semantics of predicate logic

2.4.1 Models

2.4.2 Semantic entailment

2.4.3 The semantics of equality

2.5 Undecidability of predicate logic

2.6 Expressiveness of predicate logic

2.6.1 Existential second-order logic

2.6.2 Universal second-order logic

2.7 Micromodels of software

2.7.1 State machines

2.7.2 Alma – re-visited

2.7.3 A software micromodel

2.8 Exercises

2.9 Bibliographic notes

3 Verification by model checking

3.1 Motivation for verification

3.2 Linear-time temporal logic

3.2.1 Syntax of LTL

3.2.2 Semantics of LTL

3.2.3 Practical patterns of specifications

3.2.4 Important equivalences between LTL formulas

3.2.5 Adequate sets of connectives for LTL

3.3 Model checking: systems, tools, properties

3.3.1 Example: mutual exclusion

3.3.2 The NuSMV model checker

3.3.3 Running NuSMV

3.3.4 Mutual exclusion revisited

3.3.5 The ferryman

3.3.6 The alternating bit protocol

3.4 Branching-time logic

3.4.1 Syntax of CTL

3.4.2 Semantics of computation tree logic

3.4.3 Practical patterns of specifications

3.4.4 Important equivalences between CTL formulas

3.4.5 Adequate sets of CTL connectives

3.5 CTL and the expressive powers of LTL and CTL

3.5.1 Boolean combinations of temporal formulas in CTL

3.5.2 Past operators in LTL

3.6 Model-checking algorithms

3.6.1 The CTL model-checking algorithm

3.6.2 CTL model checking with fairness

3.6.3 The LTL model-checking algorithm

3.7 The fixed-point characterisation of CTL

3.7.1 Monotone functions

3.7.2 The correctness of SATEG

3.7.3 The correctness of SATEU

3.8 Exercises

3.9 Bibliographic notes

4 Program verification

4.1 Why should we specify and verify code?

4.2 A framework for software verification

4.2.1 A core programming language

4.2.2 Hoare triples

4.2.3 Partial and total correctness

4.2.4 Program variables and logical variables

4.3 Proof calculus for partial correctness

4.3.1 Proof rules

4.3.2 Proof tableaux

4.3.3 A case study: minimal-sum section

4.4 Proof calculus for total correctness

4.5 Programming by contract

4.6 Exercises

4.7 Bibliographic notes

5 Modal logics and agents

5.1 Modes of truth

5.2 Basic modal logic

5.2.1 Syntax

5.2.2 Semantics

Equivalences between modal formulas

Valid formulas

5.3 Logic engineering

5.3.1 The stock of valid formulas

5.3.2 Important properties of the accessibility relation

5.3.3 Correspondence theory

5.3.4 Some modal logics

5.4 Natural deduction

5.5 Reasoning about knowledge in a multi-agent system

5.5.1 Some examples

5.5.2 The modal logic KT45n

5.5.3 Natural deduction for KT45n

5.5.4 Formalising the examples

5.6 Exercises

5.7 Bibliographic notes

6 Binary decision diagrams

6.1 Representing boolean functions

6.1.1 Propositional formulas and truth tables

6.1.2 Binary decision diagrams

6.1.3 Ordered BDDs

6.2 Algorithms for reduced OBDDs

6.2.1 The algorithm reduce

6.2.2 The algorithm apply

6.2.3 The algorithm restrict

6.2.4 The algorithm exists

6.2.5 Assessment of OBDDs

6.3 Symbolic model checking

6.3.1 Representing subsets of the set of states

6.3.2 Representing the transition relation

6.3.3 Implementing the functions…

6.3.4 Synthesising OBDDs

6.4 A relational mu-calculus

6.4.1 Syntax and semantics

6.5 Exercises

6.6 Bibliographic notes

Bibliography

Index

This page intentionally left blank

LOGIC IN COMPUTER SCIENCE Modelling and Reasoning about Systems

LOGIC IN COMPUTER SCIENCE Modelling and Reasoning about Systems MICHAEL HUTH Department of Computing Imperial College London, United Kingdom MARK RYAN School of Computer Science University of Birmingham, United Kingdom

CAMBRIDGE UNIVERSITY PRESS Cambridge, New York, Melbourne, Madrid, Cape Town, Singapore, São Paulo Cambridge University Press The Edinburgh Building, Cambridge CB2 8RU, UK Published in the United States of America by Cambridge University Press, New York www.cambridge.org Information on this title: www.cambridge.org/9780521543101 © Cambridge University Press 2004 This publication is in copyright. Subject to statutory exception and to the provision of relevant collective licensing agreements, no reproduction of any part may take place without the written permission of Cambridge University Press. First published in print format 2004 ISBN-13 ISBN-10 ISBN-13 ISBN-10 978-0-511-26401-6 0-511-26401-1 eBook (EBL) eBook (EBL) 978-0-521-54310-1 0-521-54310-X paperback paperback Cambridge University Press has no responsibility for the persistence or accuracy of urls for external or third-party internet websites referred to in this publication, and does not guarantee that any content on such websites is, or will remain, accurate or appropriate.

Contents Foreword to the ﬁrst edition Preface to the second edition Acknowledgements 1 Propositional logic 1.1 Declarative sentences 1.2 Natural deduction 1.2.1 Rules for natural deduction 1.2.2 Derived rules 1.2.3 Natural deduction in summary 1.2.4 Provable equivalence 1.2.5 An aside: proof by contradiction 1.3 Propositional logic as a formal language 1.4 Semantics of propositional logic 1.4.1 The meaning of logical connectives 1.4.2 Mathematical induction 1.4.3 Soundness of propositional logic 1.4.4 Completeness of propositional logic 1.5 Normal forms 1.5.1 Semantic equivalence, satisﬁability and validity 1.5.2 Conjunctive normal forms and validity 1.5.3 Horn clauses and satisﬁability 1.6 SAT solvers 1.6.1 A linear solver 1.6.2Acubicsolver 1.7 Exercises 1.8 Bibliographic notes 2 Predicate logic 2.1 The need for a richer language v page ix xi xiii 1 2 5 6 23 26 29 29 31 36 36 40 45 49 53 54 58 65 68 69 72 78 91 93 93

vi Contents 2.2 Predicate logic as a formal language 2.2.1 Terms 2.2.2 Formulas 2.2.3 Free and bound variables 2.2.4 Substitution 2.3 Proof theory of predicate logic 2.3.1 Natural deduction rules 2.3.2 Quantiﬁer equivalences 2.4 Semantics of predicate logic 2.4.1 Models 2.4.2 Semantic entailment 2.4.3 The semantics of equality 2.5 Undecidability of predicate logic 2.6 Expressiveness of predicate logic 2.6.1 Existential second-order logic 2.6.2 Universal second-order logic 2.7 Micromodels of software 2.7.1 State machines 2.7.2 Alma – re-visited 2.7.3 A software micromodel 2.8 Exercises 2.9 Bibliographic notes 3 Veriﬁcation by model checking 3.1 Motivation for veriﬁcation 3.2 Linear-time temporal logic 3.2.1 Syntax of LTL 3.2.2 Semantics of LTL 3.2.3 Practical patterns of speciﬁcations 3.2.4 Important equivalences between LTL formulas 3.2.5 Adequate sets of connectives for LTL 3.3 Model checking: systems, tools, properties 3.3.1 Example: mutual exclusion 3.3.2TheNuSMVmodelchecker 3.3.3 Running NuSMV 3.3.4 Mutual exclusion revisited 3.3.5 The ferryman 3.3.6 The alternating bit protocol 3.4 Branching-time logic 3.4.1 Syntax of CTL 191 98 99 100 102 104 107 107 117 122 123 129 130 131 136 139 140 141 142 146 148 157 170 172 172 175 175 178 183 184 186 187 187 194 195 199 203 207 208

分享到：

赞收藏

资料库

Logic in Computer Science.pdf

相关推荐

课程资源

热门标签

最新资料