Mathematical logic in computer science

This book is devoted to the issues of logic, which form the basis of education of every computer scientist and engineer using computer methods.
It discusses the propositional calculus, first order logic, logic programming, specification and verification of programs, and temporal logic. All presented implementations were made in Prolog.
It is an excellent textbook, with great didactic qualities, written with great knowledge of the subject, and in addition understandable. In each chapter there are many examples illustrating the concepts and methods discussed, as well as exercises with varying degrees of difficulty.
The book is intended for students of the first years of study in the field of IT. It will also be used by teaching staff conducting classes on applied logic.

Table of Contents

Preface

1. Introduction

1.1. The origins of mathematical logic
1.2. Sentence calculus
1.3. Predicate calculus
1.4. Proving theorems and programming in logic
1.5. Logic systems
1.6. Exercise

2. The propositional calculus: formulas, models, semantic tables

2.1. Logic operators
2.2. Formulas for propositional calculus
2.3. interpretations
2.4. Logical equivalence
2.5. Satisfaction, truth and logical consequences
2.6. Semantic table method
2.7. Correctness and fullness
2.8. Implementation in Prolog
2.9. exercises

3. Sentence calculus: command systems

3.1. Deriving formulas
3.2. Gentzen system
3.3. The Hilbert system
3.4. The correctness and completeness of the Hilbert system
3.5. A verifier of evidence in Prolog
3.6. Variations of command systems *
3.7. exercises

4. The propositional calculus: resolution and diagrams of binary decisions

4.1. Resolution
4.2. Diagrams of binary decisions (DBD)
4.3. Algorithms operating on binary decision diagrams
4.4. Complexity*
4.5. exercises

5. Predicate calculus: formulas, models, semantic tables

5.1. Relations and predicates
5.2. Predicate calculus formulas
5.3. interpretations
5.4. Logical equivalence
5.5. Semantic table method
5.6. Implementation in Prolog
5.7. Finite and infinite models *
5.8. Decidability
5.9. exercises

6. Predicate calculus: command systems

6.1. Gentzen system
6.2. The Hilbert system
6.3. Implementation in Prolog
6.4. Complete and decidable theories *
6.5. exercises

7. Predicate calculus: resolution

7.1. Functions and terms
7.2. Form clause formulas
7.3. Herbrand models
7.4. Herbrand's theorem *
7.5. Resolution for established clauses
7.6. substitutions
7.7. Reconciliation
7.8. Resolution
7.9. exercises

8. Programming in logic

8.1. Formulas as programs
8.2. SLD-resolution
8.3. Prologue
8.4. Concurrent programming in logic *
8.5. Programming in logic with constraints *
8.6. exercises

9. Programs: semantics and verification

9.1. Introduction
9.2. Semantics of programming languages
9.3. HL command system
9.4. Verification of programs
9.5. Synthesis of programs
9.6. The correctness and completeness of the HL system
9.7. exercises

10. Programs: formal specifications in Z notation

10.1. Example: traffic light
10.2. Notation Z
10.3. Example: semantic table
10.4. exercises

11. Temporal logic: formulas, models, semantic tables

11.1. Introduction
11.2. Syntax and semantics
11.3. Time models
11.4. Semantic table method
11.5. Implementation of the semantic table method in Prolog
11.6. exercises

12. Temporal logic: command and application systems

12.1. Command system L
12.2. Correctness and fullness of L *
12.3. Other temporal logics *
12.4. Specifications and verification of programs *
12.5. Model verification *
12.6. exercises

A. Set theory
A.1. Finite and infinite sets
A.2. Operations on sets
A.3. Ordered sets
A.4. Relations and functions
A.5. Harvesting power
A.6. Proof of harvest properties

B. Further reading

Bibliography
List of symbols
Index