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.2 Predicate 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.