Mathematical Logic for Computer Science

1 Introduction.- 1.1 The origins of mathematical logic.- 1.2 Propositional calculus.- 1.3 Predicate calculus.- 1.4 Theorem proving and logic programming.- 1.5 Systems of logic.- 1.6 Exercise.- 2 Propositional Calculus: Formulas, Models, Tableaux.- 2.1 Boolean Operators.- 2.2 Propositional formulas.- 2.3 Interpretation.- 2.4 Logical equivalence and Substitution.- 2.5 Satisfiability, validity and consequence.- 2.6 Semantic tableaux.- 2.7 Soundness and completeness.- 2.8 Implementationp.- 2.9 Exercises.- 3 Propositional Calculus: Deductive Systems.- 3.1 Deductive proofs.- 3.2 The Gentzen System G.- 3.3 The Hubert System H.- 3.4 Soundness and completeness of H.- 3.5 A proof checkerp.- 3.6 Variant forms of the deductive Systems*.- 3.7 Exercises.- 4 Propositional Calculus: Resolution and BDDs.- 4.1 Resolution.- 4.2 Binary decision diagrams (BDDs).- 4.3 Algorithms on BDDs.- 4.4 Complexity*.- 4.5 Exercises.- 5 Predicate Calculus: Formulas, Models, Tableaux.- 5.1 Relations and predicates.- 5.2Predicate formulas.- 5.3 Interpretation.- 5.4 Logical equivalence and Substitution.- 5.5 Semantic tableaux.- 5.6 Implementationp.- 5.7 Finite and infinite modeis*.- 5.8 Decidability*.- 5.9 Exercises.- 6 Predicate Calculus: Deductive Systems.- 6.1 The Gentzen system G.- 6.2 The Hubert system H.- 6.3 Implementationp.- 6.4 Complete and decidable theories*.- 6.5 Exercises.- 7 Predicate Calculus: Resolution.- 7.1 Functions and terms.- 7.2 Clausal form.- 7.3 Herbrand modeis.- 7.4 Herbrand's Theorem*.- 7.5 Ground resolution.- 7.6 Substitution.- 7.7 Unification.- 7.8 General resolution.- 7.9 Exercises.- 8 Logic Programming.- 8.1 Formulas as programs.- 8.2 SLD-resolution.- 8.3 Prolog.- 8.4 Concurrent logic programming*.- 8.5 Constraint logic programming*.- 8.6 Exercises.- 9 Programs: Semantics and Verification.- 9.1 Introduction.- 9.2 Semantics of programming languages.- 9.3 The deductive system HL.- 9.4 Program verification.- 9.5 Program synthesis.- 9.6 Soundness and completeness of HL.- 9.7 Exercises.- 10 Programs: Formal Specification with Z.- 10.1 Case study: a traflfic signal.- 10.2 The Z notation.- 10.3 Case study: semantic tableaux.- 10.4 Exercises.- 11 Temporal Logic: Formulas, Models, Tableaux.- 11.1 Introduction.- 11.2 Syntax and semantics.- 11.3 Models oftime.- 11.4 Semantic tableaux.- 11.5 Implementation of semantic tableauxp.- 11.6 Exercises.- 12 Temporal Logic: Deduction and Applications.- 12.1 The deductive system L.- 12.2 Soundness and completeness of L*.- 12.3 Other temporal logics*.- 12.4 Specification and verification of programs*.- 12.5 Model checking*.- 12.6 Exercises.- A Set Theory.- B Further Reading.- Index of Symbols.