Logic in Computer Science
Subtitle: Modelling and Reasoning about Systems
Edition: 2 edition
Publisher: Cambridge University Press
Published: August 30, 2004
Language: eng
Format: Paperback
Number of pages: 440
ISBN-13: 9780521543101
Subjects: Computer architecture & logic design; Mathematical theory of computation; Systems analysis & design; Logic Design; Computer logic; Computers; Computers - General Information; Computer Books: General; Logic programming (Computer sc; Computer Science; Computers / Programming / Software Development; Logic programming (Computer science)
Table of contents: title: Foreword to the First Edition
pagenum: ix; title: Preface to the Second Edition
pagenum: xi; title: Acknowledgements
pagenum: xiii; label: 1
title: Propositional Logic
pagenum: 1; label: 1.1
title: Declarative Sentences
pagenum: 2; label: 1.2
title: Natural Deduction
pagenum: 5; label: 1.2.1
title: Rules for Natural Deduction
pagenum: 6; label: 1.2.2
title: Derived Rules
pagenum: 23; label: 1.2.3
title: Natural Deduction in Summary
pagenum: 26; label: 1.2.4
title: Provable Equivalence
pagenum: 29; label: 1.2.5
title: An Aside: Proof by Contradiction
pagenum: 29; label: 1.3
title: Propositional Logic as a Formal Language
pagenum: 31; label: 1.4
title: Semantics of Propositional Logic
pagenum: 36; label: 1.4.1
title: The Meaning of Logical Connectives
pagenum: 36; label: 1.4.2
title: Mathematical Induction
pagenum: 40; label: 1.4.3
title: Soundness of Propositional Logic
pagenum: 45; label: 1.4.4
title: Completeness of Propositional Logic
pagenum: 49; label: 1.5
title: Normal Forms
pagenum: 53; label: 1.5.1
title: Semantic Equivalence, Satisfiability and Validity
pagenum: 54; label: 1.5.2
title: Conjunctive Normal Forms and Validity
pagenum: 58; label: 1.5.3
title: Horn Clauses and Satisfiability
pagenum: 65; label: 1.6
title: SAT Solvers
pagenum: 68; label: 1.6.1
title: A Linear Solver
pagenum: 69; label: 1.6.2
title: A Cubic Solver
pagenum: 72; label: 1.7
title: Exercises
pagenum: 78; label: 1.8
title: Bibliographic Notes
pagenum: 91; label: 2
title: Predicate Logic
pagenum: 93; label: 2.1
title: The Need for a Richer Language
pagenum: 93; label: 2.2
title: Predicate Logic as a Formal Language
pagenum: 98; label: 2.2.1
title: Terms
pagenum: 99; label: 2.2.2
title: Formulas
pagenum: 100; label: 2.2.3
title: Free and Bound Variables
pagenum: 102; label: 2.2.4
title: Substitution
pagenum: 104; label: 2.3
title: Proof Theory of Predicate Logic
pagenum: 107; label: 2.3.1
title: Natural Deduction Rules
pagenum: 107; label: 2.3.2
title: Quantifier Equivalences
pagenum: 117; label: 2.4
title: Semantics of Predicate Logic
pagenum: 122; label: 2.4.1
title: Models
pagenum: 123; label: 2.4.2
title: Semantic Entailment
pagenum: 129; label: 2.4.3
title: The Semantics of Equality
pagenum: 130; label: 2.5
title: Undecidability of Predicate Logic
pagenum: 131; label: 2.6
title: Expressiveness of Predicate Logic
pagenum: 136; label: 2.6.1
title: Existential Second-Order Logic
pagenum: 139; label: 2.6.2
title: Universal Second-Order Logic
pagenum: 140; label: 2.7
title: Micromodels of Software
pagenum: 141; label: 2.7.1
title: State Machines
pagenum: 142; label: 2.7.2
title: Alma - Re-Visited
pagenum: 146; label: 2.7.3
title: A Software Micromodel
pagenum: 148; label: 2.8
title: Exercises
pagenum: 157; label: 2.9
title: Bibliographic Notes
pagenum: 170; label: 3
title: Verification by Model Checking
pagenum: 172; label: 3.1
title: Motivation for Verification
pagenum: 172; label: 3.2
title: Linear-Time Temporal Logic
pagenum: 175; label: 3.2.1
title: Syntax of LTL
pagenum: 175; label: 3.2.2
title: Semantics of LTL
pagenum: 178; label: 3.2.3
title: Practical Patterns of Specifications
pagenum: 183; label: 3.2.4
title: Important Equivalences Between LTL Formulas
pagenum: 184; label: 3.2.5
title: Adequate Sets of Connectives for LTL
pagenum: 186; label: 3.3
title: Model Checking: Systems, Tools, Properties
pagenum: 187; label: 3.3.1
title: Example: Mutual Exclusion
pagenum: 187; label: 3.3.2
title: The NuSMV Model Checker
pagenum: 191; label: 3.3.3
title: Running NuSMV
pagenum: 194; label: 3.3.4
title: Mutual Exclusion Revisited
pagenum: 195; label: 3.3.5
title: The Ferryman
pagenum: 199; label: 3.3.6
title: The Alternating Bit Protocol
pagenum: 203; label: 3.4
title: Branching-Time Logic
pagenum: 207; label: 3.4.1
title: Syntax of CTL
pagenum: 208; label: 3.4.2
title: Semantics of CTL
pagenum: 211; label: 3.4.3
title: Practical Patterns of Specifications
pagenum: 215; label: 3.4.4
title: Important Equivalences Between CTL Formulas
pagenum: 215; label: 3.4.5
title: Adequate Sets of CTL Connectives
pagenum: 216; label: 3.5
title: CTL* and the Expressive Powers of LTL and CTL
pagenum: 217; label: 3.5.1
title: Boolean Combinations of Temporal Formulas in CTL
pagenum: 220; label: 3.5.2
title: Past Operators in LTL
pagenum: 221; label: 3.6
title: Model-Checking Algorithms
pagenum: 221; label: 3.6.1
title: The CTL Model-Checking Algorithm
pagenum: 222; label: 3.6.2
title: CTL Model Checking with Fairness
pagenum: 230; label: 3.6.3
title: The LTL Model-Checking Algorithm
pagenum: 232; label: 3.7
title: The Fixed-Point Characterisation of CTL
pagenum: 238; label: 3.7.1
title: Monotone Functions
pagenum: 240; label: 3.7.2
title: The Correctness of SATEG
pagenum: 242; label: 3.7.3
title: The Correctness of SATEU
pagenum: 243; label: 3.8
title: Exercises
pagenum: 245; label: 3.9
title: Bibliographic Notes
pagenum: 254; label: 4
title: Program Verification
pagenum: 256; label: 4.1
title: Why Should We Specify and Verify Code?
pagenum: 257; label: 4.2
title: A Framework for Software Verification
pagenum: 258; label: 4.2.1
title: A Core Programming Language
pagenum: 259; label: 4.2.2
title: Hoare Triples
pagenum: 262; label: 4.2.3
title: Partial and Total Correctness
pagenum: 265; label: 4.2.4
title: Program Variables and Logical Variables
pagenum: 268; label: 4.3
title: Proof Calculus for Partial Correctness
pagenum: 269; label: 4.3.1
title: Proof Rules
pagenum: 269; label: 4.3.2
title: Proof Tableaux
pagenum: 273; label: 4.3.3
title: A Case Study: Minimal-Sum Section
pagenum: 287; label: 4.4
title: Proof Calculus for Total Correctness
pagenum: 292; label: 4.5
title: Programming by Contract
pagenum: 296; label: 4.6
title: Exercises
pagenum: 299; label: 4.7
title: Bibliographic Notes
pagenum: 304; label: 5
title: Modal Logics and Agents
pagenum: 306; label: 5.1
title: Modes of Truth
pagenum: 306; label: 5.2
title: Basic Modal Logic
pagenum: 307; label: 5.2.1
title: Syntax
pagenum: 307; label: 5.2.2
title: Semantics
pagenum: 308; label: 5.3
title: Logic Engineering
pagenum: 316; label: 5.3.1
title: The Stock of Valid Formulas
pagenum: 317; label: 5.3.2
title: Important Properties of the Accessibility Relation
pagenum: 320; label: 5.3.3
title: Correspondence Theory
pagenum: 322; label: 5.3.4
title: Some Modal Logics
pagenum: 326; label: 5.4
title: Natural Deduction
pagenum: 328; label: 5.5
title: Reasoning About Knowledge in a Multi-Agent System
pagenum: 331; label: 5.5.1
title: Some Examples
pagenum: 332; label: 5.5.2
title: The Modal Logic KT45n
pagenum: 335; label: 5.5.3
title: Natural Deduction for KT45n
pagenum: 339; label: 5.5.4
title: Formalising the Examples
pagenum: 342; label: 5.6
title: Exercises
pagenum: 350; label: 5.7
title: Bibliographic Notes
pagenum: 356; label: 6
title: Binary Decision Diagrams
pagenum: 358; label: 6.1
title: Representing Boolean Functions
pagenum: 358; label: 6.1.1
title: Propositional Formulas and Truth Tables
pagenum: 359; label: 6.1.2
title: Binary Decision Diagrams
pagenum: 361; label: 6.1.3
title: Ordered BDDs
pagenum: 366; label: 6.2
title: Algorithms for Reduced OBDDs
pagenum: 372; label: 6.2.1
title: The Algorithm Reduce
pagenum: 372; label: 6.2.2
title: The Algorithm Apply
pagenum: 373; label: 6.2.3
title: The Algorithm Restrict
pagenum: 377; label: 6.2.4
title: The Algorithm Exists
pagenum: 377; label: 6.2.5
title: Assessment of OBDDs
pagenum: 380; label: 6.3
title: Symbolic Model Checking
pagenum: 382; label: 6.3.1
title: Representing Subsets of the Set of States
pagenum: 383; label: 6.3.2
title: Representing the Transition Relation
pagenum: 385; label: 6.3.3
title: Implementing the Functions Pre- and Post-
pagenum: 387; label: 6.3.4
title: Synthesising OBDDs
pagenum: 387; label: 6.4
title: A Relational Mu-Calculus
pagenum: 390; label: 6.4.1
title: Syntax and Semantics
pagenum: 390; label: 6.4.2
title: Coding CTL Models and Specifications
pagenum: 393; label: 6.5
title: Exercises
pagenum: 398; label: 6.6
title: Bibliographic Notes
pagenum: 413; title: Bibliography
pagenum: 414; title: Index
pagenum: 418