Book:M. Ben-Ari/Mathematical Logic for Computer Science
Jump to navigation
Jump to search
M. Ben-Ari: Mathematical Logic for Computer Science
Published $\text {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
Further Editions
- 2001: M. Ben-Ari: Mathematical Logic for Computer Science (2nd ed.)
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.)
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$
Source work progress
- 1993: M. Ben-Ari: Mathematical Logic for Computer Science ... (previous) ... (next): Chapter $2$: Propositional Calculus: $\S 2.4$: Logical equivalence and substitution: Definition $2.4.5$