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

## M. Ben-Ari: Mathematical Logic for Computer Science

Published $\text {1993}$, Prentice Hall

ISBN 0-13-564139-X.

### 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.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

Next

## Errata

### Binary Logical Connective is Self-Inverse iff Exclusive Or

Chapter $2$: Propositional Calculus: $2.1$. Boolean Operations

Let $\circ$ be a binary logical connective.

Then:

$\paren {p \circ q} \circ q \dashv \vdash p$

if and only if $\circ$ is the exclusive or operator.

$\mathsf{XOR}$ is also essential since it is the only operator having an inverse, namely itself
$\paren {p \oplus q} \oplus q = p$