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.

This is a mathematics textbook with theorems and proofs. The choice of topics has been guided by the needs of computer science students. The method of semantic tableaux provides an elegant way to teach logic that is both theoretically sound and yet sufficiently elementary for undergraduates. In order to provide a balanced treatment of logic, tableaux are related to deductive proof systems. The book presents various logical systems and contains exercises. Still further, Prolog source code is available on an accompanying Web site. The author is an Associate Professor at the Department of Science Teaching, Weizmann Institute of Science.