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

## M. Ben-Ari: *Mathematical Logic for Computer Science, 1st ed.*

Published $1993$, **Prentice Hall**

- ISBN 0-13-564139-X.

### Subject Matter

### Contents

**Preface**

**1. Introduction**- 1.1 The origins of mathematical logic
- 1.2 Propositional and predicate calculus
- 1.3 Theorem provers and logic programming
- 1.4 Non-standard logics

**2. Propositional calculus**- 2.1 Boolean operators
- 2.2 Propositional formulas
- 2.3 Boolean interpretations
- 2.4 Logical equivalence and substitution
- 2.5 Satisfiability, validity and consequence
- 2.6 Semantic tableaux
- 2.7 Deductive proofs
- 2.8 Gentzen systems
- 2.9 Hilbert systems
- 2.10 Resolution
- 2.11 Variant forms of the deductive systems
^{*} - 2.12 Complexity
^{*} - 2.13 Exercises

**3. Predicate calculus**- 3.1 Relations and predicates
- 3.2 predicate formulas
- 3.3 Interpretations
- 3.4 Logical equivalence and substitution
- 3.5 Semantic tableaux
- 3.6 Deductive proofs
- 3.7 Functions and terms
- 3.8 Clausal form
- 3.9 Herbrand models
- 3.10 Finite and infinite models
^{*} - 3.11 Solvable cases of the decision problem
^{*} - 3.12 Exercises

**4. Resolution and logic programming**- 4.1 Ground resolution
- 4.2 Substitution
- 4.3 Unification
- 4.4 General resolution
- 4.5 Theories and theorem proving
- 4.6 Logic programming
- 4.7 Prolog
- 4.8 Parallel logic programming
^{*} - 4.9 Complete and decidable theories
^{*} - 4.10 Exercises

**5. Temporal logic**- 5.1 Introduction
- 5.2 Syntax and semantics
- 5.3 A deductive system for linear PTL
- 5.4 Semantic tableaux
- 5.5 Soundness and completeness
- 5.6 Applications of temporal logic
^{*} - 5.7 Extensions of temporal logic
^{*} - 5.8 Exercises

**6. Formalization of programs**- 6.1 Introduction
- 6.2 Axiomatisation of a language
- 6.3 Proving programs
- 6.4 Formal specification with $Z$
- 6.5 Exercises

**7. Further reading**- 7.1 Mathematical logic
- 7.2 Complexity
- 7.3 Resolution and logic programming
- 7.4 Temporal logic
- 7.5 Formalization of programs

**Bibliography**

**Appendices**

**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

**B. Algorithm implementation**

**C. Hints**

**Index**