Logic in Computer Science
Subtitle: Modelling and Reasoning about Systems
Publisher: Cambridge University Press
Published: November 1, 1999
Language: eng
Format: Paperback
Number of pages: 405
ISBN-13: 9780521656023
Subjects: Computer Communications & Networking; Mathematical theory of computation; Software engineering; General; Computer logic; Computers; Computers - General Information; Computer Books: General; Logic Design; Computer Science; Computers / Programming / Software Development
Table of contents: title: Foreword
pagenum: ix; title: Preface
pagenum: xi; title: Acknowledgments
pagenum: xviii; label: 1
title: Propositional Logic
pagenum: 1; label: 1.1
title: Declarative Sentences
pagenum: 2; label: 1.2
title: Natural Deduction
pagenum: 6; label: 1.2.1
title: Rules for Natural Deduction
pagenum: 7; label: 1.2.2
title: Derived Rules
pagenum: 28; label: 1.2.3
title: Natural Deduction in Summary
pagenum: 30; label: 1.2.4
title: Provable Equivalence
pagenum: 33; label: 1.2.5
title: An Aside: Proof by Contradiction
pagenum: 34; label: 1.3
title: Propositional Logic as a Formal Language
pagenum: 38; label: 1.4
title: Semantics of Propositional Logic
pagenum: 45; label: 1.4.1
title: The Meaning of Logical Connectives
pagenum: 45; label: 1.4.2
title: Mathematical Induction
pagenum: 51; label: 1.4.3
title: Soundness of Propositional Logic
pagenum: 56; label: 1.4.4
title: Completeness of Propositional Logic
pagenum: 61; label: 1.5
title: Normal Forms
pagenum: 69; label: 1.5.1
title: Semantic Equivalence, Satisfiability and Validity
pagenum: 69; label: 1.5.2
title: Conjunctive Normal Forms and Validity
pagenum: 76; label: 1.5.3
title: Horn Clauses and Satisfiability
pagenum: 84; label: 1.6
title: Bibliographic Notes
pagenum: 89; label: 2
title: Predicate Logic
pagenum: 90; label: 2.1
title: The Need for a Richer Language
pagenum: 90; label: 2.2
title: Predicate Logic as a Formal Language
pagenum: 96; label: 2.2.1
title: Terms
pagenum: 96; label: 2.2.2
title: Formulas
pagenum: 98; label: 2.2.3
title: Free and Bound Variables
pagenum: 103; label: 2.2.4
title: Substitution
pagenum: 105; label: 2.3
title: Proof Theory of Predicate Logic
pagenum: 109; label: 2.3.1
title: Natural Deduction Rules
pagenum: 109; label: 2.3.2
title: Quantifier Equivalences
pagenum: 120; label: 2.4
title: Semantics of Predicate Logic
pagenum: 128; label: 2.4.1
title: Models
pagenum: 129; label: 2.4.2
title: Semantic Entailment
pagenum: 136; label: 2.4.3
title: The Semantics of Equality
pagenum: 138; label: 2.5
title: Undecidability of Predicate Logic
pagenum: 140; label: 2.6
title: Bibliographic Notes
pagenum: 147; label: 3
title: Verification by Model Checking
pagenum: 148; label: 3.1
title: Motivation for Verification
pagenum: 148; label: 3.2
title: The Syntax of Computation Tree Logic
pagenum: 152; label: 3.3
title: Semantics of Computation Tree Logic
pagenum: 156; label: 3.3.1
title: Practical Patterns of Specifications
pagenum: 165; label: 3.3.2
title: Important Equivalences Between CTL Formulas
pagenum: 166; label: 3.4
title: Example: Mutual Exclusion
pagenum: 169; label: 3.4.1
title: The First Modelling Attempt
pagenum: 170; label: 3.4.2
title: The Second Modelling Attempt
pagenum: 171; label: 3.5
title: A Model-Checking Algorithm
pagenum: 172; label: 3.5.1
title: The Labelling Algorithm
pagenum: 173; label: 3.5.2
title: The Pseudo-Code of the Model Checking Algorithm
pagenum: 177; label: 3.5.3
title: The 'State Explosion' Problem
pagenum: 178; label: 3.6
title: The SMV System
pagenum: 181; label: 3.6.1
title: Modules in SMV
pagenum: 183; label: 3.6.2
title: Synchronous and Asynchronous Composition
pagenum: 184; label: 3.6.3
title: Mutual Exclusion Revisited
pagenum: 185; label: 3.6.4
title: The Alternating Bit Protocol
pagenum: 187; label: 3.7
title: Model Checking with Fairness
pagenum: 193; label: 3.8
title: Alternatives and Extensions of CTL
pagenum: 196; label: 3.8.1
title: Linear-Time Temporal Logic
pagenum: 196; label: 3.8.2
title: CTL*
pagenum: 198; label: 3.8.3
title: The Expressive Power of CTL
pagenum: 201; label: 3.9
title: The Fixed-Point Characterisation of CTL
pagenum: 203; label: 3.9.1
title: Monotone Functions
pagenum: 205; label: 3.9.2
title: The Correctness of SatEG
pagenum: 208; label: 3.9.3
title: The Correctness of SatEU
pagenum: 210; label: 3.10
title: Bibliographic Notes
pagenum: 214; label: 4
title: Program Verification
pagenum: 216; label: 4.1
title: Why Should We Specify and Verify Code?
pagenum: 217; label: 4.2
title: A Framework for Software Verification
pagenum: 218; label: 4.2.1
title: A Core Programming Language
pagenum: 220; label: 4.2.2
title: Hoare Triples
pagenum: 223; label: 4.2.3
title: Partial and Total Correctness
pagenum: 226; label: 4.2.4
title: Program Variables and Logical Variables
pagenum: 229; label: 4.3
title: Proof Calculus for Partial Correctness
pagenum: 230; label: 4.3.1
title: Proof Rules
pagenum: 230; label: 4.3.2
title: Proof Tableaux
pagenum: 234; label: 4.3.3
title: A Case Study: Minimal-Sum Section
pagenum: 252; label: 4.4
title: Proof Calculus for Total Correctness
pagenum: 257; label: 4.5
title: Bibliographic Notes
pagenum: 260; label: 5
title: Modal Logics and Agents
pagenum: 261; label: 5.1
title: Modes of Truth
pagenum: 261; label: 5.2
title: Basic Modal Logic
pagenum: 262; label: 5.2.1
title: Syntax
pagenum: 262; label: 5.2.2
title: Semantics
pagenum: 263; label: 5.3
title: Logic Engineering
pagenum: 273; label: 5.3.1
title: The Stock of Valid Formulas
pagenum: 274; label: 5.3.2
title: Important Properties of the Accessibility Relation
pagenum: 277; label: 5.3.3
title: Correspondence Theory
pagenum: 280; label: 5.3.4
title: Some Modal Logics
pagenum: 284; label: 5.3.5
title: Semantic Entailment
pagenum: 288; label: 5.4
title: Natural Deduction
pagenum: 289; label: 5.5
title: Reasoning About Knowledge in a Multi-Agent System
pagenum: 293; label: 5.5.1
title: Some Examples
pagenum: 293; label: 5.5.2
title: The Modal Logic KT45^n
pagenum: 296; label: 5.5.3
title: Natural Deduction for KT45^n
pagenum: 302; label: 5.5.4
title: Formalising the Examples
pagenum: 304; label: 5.6
title: Bibliographic Notes
pagenum: 314; label: 6
title: Binary Decision Diagrams
pagenum: 316; label: 6.1
title: Representing Boolean Functions
pagenum: 316; label: 6.1.1
title: Propositional Formulas and Truth Tables
pagenum: 317; label: 6.1.2
title: Binary Decision Diagrams
pagenum: 319; label: 6.1.3
title: Ordered BDDs
pagenum: 326; label: 6.2
title: Algorithms for Reduced OBDDs
pagenum: 334; label: 6.2.1
title: The Algorithm Reduce
pagenum: 334; label: 6.2.2
title: The Algorithm Apply
pagenum: 336; label: 6.2.3
title: The Algorithm Restrict
pagenum: 342; label: 6.2.4
title: The Algorithm Exists
pagenum: 344; label: 6.2.5
title: Assessment of OBDDs
pagenum: 348; label: 6.3
title: Symbolic Model Checking
pagenum: 351; label: 6.3.1
title: Representing Subsets of the Set of States
pagenum: 351; label: 6.3.2
title: Representing the Transition Relation
pagenum: 354; label: 6.3.3
title: Implementing the Functions preg and prev
pagenum: 355; label: 6.3.4
title: Synthesising OBDDs
pagenum: 357; label: 6.4
title: A Relational Mu-Calculus
pagenum: 361; label: 6.4.1
title: Syntax and Semantics
pagenum: 362; label: 6.4.2
title: Coding CTL Models and Specifications
pagenum: 366; label: 6.5
title: Bibliographic Notes
pagenum: 374; title: Bibliography
pagenum: 375; title: Index
pagenum: 378