Preface
Students of science and engineering are required to study mathematics during their first years at a university. Traditionally, they concentrate on calculus, linear algebra and differential equations, but in computer science and engineering, logic, combinatorics and discrete mathematics are more appropriate. Logic is particularly important because it is the mathematical basis of software: it is used to formalize the semantics of programming languages and the specification of programs, and to verify the correctness of programs.
Mathematical Logic for Computer Science is a mathematics textbook, just as a first-year calculus text is a mathematics textbook. A scientist or engineer needs more than just a facility for manipulating formulas and a firm foundation in mathematics is an excellent defense against technological obsolescence. Tempering this requirement for mathematical competence is the realization that applications use only a fraction of the theoretical results. Just as the theory of calculus can be taught to students of engineering without the full generality of measure theory, students of computer science need not be taught the full generality of uncountable structures. Fortunately (as shown by Raymond M. Smullyan), tableaux provide an elegant way to teach mathematical logic that is both theoretically sound and yet sufficiently elementary for the undergraduate.
The book is intended for undergraduate computer science students. No specific mathematical knowledge is assumed aside from informal set theory which is summarized in an appendix, but elementary knowledge of concepts from computer science (graphs, languages, programs) are used. Prolog implementations of many of the algorithms are given; for a computer science student, the study of a concrete program can reinforce the study of an abstract algorithm. An ideal course in logic would supplement the theory in this book with practical study of logic programming.
My approach can be characterized as broad, elementary and rigorous: I want to cover many topics rigorously, but I have chosen elementary material, generally the minimal subset of a logic that can be profitably studied. Examples are: the predicate calculus without equality, a future fragment of temporal logic and partial rather than total correctness. The student who has learned the results and techniques in these elementary cases will be well-prepared to study the more general systems in advanced courses.
Chapter 1 is introductory and surveys the topics in the book. Appendix A summarizes the elementary set theory that the reader should know, and Appendix B contains a guide to the literature. The rest of the book covers five main topics:
- Propositional calculus (Chapters 2, 3, 4).
- Predicate calculus (Chapters 5, 6).
- Resolution and logic programming (Chapters 7, 8).
- Program specification and verification (Chapters 9, 10).
- Temporal logic (Chapters 11, 12).
The first two topics form the core of classical mathematical logic, though I have augmented them with algorithms and programs, and material of interest to computer scientists. The other three topics are chosen for their specific relevance in modern computer science.
The general progression in each main topic is: syntax and semantics of formulas, semantic tableaux, deductive systems and algorithms. While many modern textbooks are heavily weighted in favor of algorithmic semantic methods, I have tried to give equal time to syntactic deduction. Deduction is still the language of mathematical reasoning and is the only fall-back when semantic methods fail.
The propositional and predicate calculi are the central topics in logic and should be taught in any course. The other three topics are independent of each other and the instructor can select or rearrange the topics as desired. Sections marked * contain advanced material that may be skipped in lower-level undergraduate classes, as well as interesting results presented without proof that are beyond the scope of this book. Sections marked P contain the Prolog programs. The printed programs are only fragments; the full source code of the programs (including routines for input-output and testing) is available online The programs have been run on the free implementation SWI Prolog but should run on any implementation of the Prolog standard.
The second edition has been totally rewritten. Major additions are sections on binary decision diagrams, constraint logic programming and the completeness of Hoare logic. One curiosity: I had used Fermat's Last Theorem as an example of a formula whose truth is not known. Since then, Andrew Wiles has proved the theorem! I have chosen to replace it by Goldbach's conjecture.
Table of Contents
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
2.9 Exercises
3 Propositional Calculus: Deductive Systems
3.1 Deductive proofs
3.2 The Gentzen system G
3.3 The Hilbert system H
3.4 Soundness and completeness of H
3.5 A proof checker
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 (BDD)
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
5.7 Finite and infinite models
5.8 Decidability
5.9 Exercises
6 Predicate Calculus: Deductive Systems
6.1 The Gentzen system G
6.2 The Hilbert system H
6.3 Implementation
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 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 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
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