# Book:M. Ben-Ari/Mathematical Logic for Computer Science/Second Edition

## M. Ben-Ari: Mathematical Logic for Computer Science (2nd Edition)

Published $\text {1993}$, Springer Verlag

ISBN 1-85233-319-7

### Contents

Preface
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 Interpretations
2.4 Logical equivalence and substitution
2.5 Satisfiability, validity and consequence
2.6 Semantic tableaux
2.7 Soundness and completeness
2.8 Implementation$^P$
2.9 Exercises
3 Propositional Calculus: Deductive Systems
3.1 Deductive proofs
3.2 The Gentzen system $\mathcal G$
3.3 The Hilbert system $\mathcal H$
3.4 Soundness and completeness of $\mathcal H$
3.5 A proof checker$^P$
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 Interpretations
5.4 Logical equivalence and substitution
5.5 Semantic tableaux
5.6 Implementation$^P$
5.7 Finite and infinite models$^*$
5.8 Decidability$^*$
5.9 Exercises
6 Predicate Calculus: Deductive Systems
6.1 The Gentzen system $\mathcal G$
6.2 The Hilbert system $\mathcal H$
6.3 Implementation$^P$
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 models
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 $\mathcal{HL}$
9.4 Program verification
9.5 Program synthesis
9.6 Soundness and completeness of $\mathcal{HL}$
9.7 Exercises
10 Programs: Formal Specification with Z
10.1 Case study: a traffic 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 of time
11.4 Semantic tableaux
11.5 Implementation of semantic tableaux$^P$
11.6 Exercises
12 Temporal Logic: Deduction and Applications
12.1 The deductive system $\mathcal L$
12.2 Soundness and completeness of $\mathcal L^*$
12.3 Other temporal logics$^*$
12.4 Specification and verification of programs$^*$
12.5 Model checking$^*$
12.6 Exercises
A Set Theory
A.1 Finite and infinite sets
A.2 Set operators
A.3 Ordered sets
A.4 Relations and functions
A.5 Cardinality
A.6 Proving properties of sets