This is a rewritten version of a book first published in 1993. It is intended for undergraduate computer science students, using an approach that the author promises as broad, elementary and rigorous.

The book is organized in three parts: propositional calculus, predicate calculus and computer oriented logics. The expositions of propositional and predicate calculi follow the same lines: semantic tableaux (chapters 2 and 5), formalization in Gentzen and Hilbert deductive systems (chapters 3 and 6) and algorithms for resolution (chapters 4 and 7).

The author has made three deliberate choices in this focus and presentation:

1. an introduction of the calculi through the semantic tableaux in the sense of Smullyan, satisfiability of a formula being the primitive notion. Recall that from the tableaux, one may slide towards the deductive systems (as in this book) or towards model theory (a theme only touched upon through the statement of the Skolem Lowenheim theorem, though one cannot deal with all subjects).
2. a concise but explicit reference to deductive systems, although they do not lend themselves to algorithmic developments
3. a detailed treatment of the propositional calculus used to expose the main features of the resolution. This approach is unusual but pedagogically very valuable: the task is largely simplified when one goes into the real resolution - the resolution for predicate calculus (see chapter 7).

There is another advantage to using propositional calculus: the creation of a tableau and the conversion to conjunctive normal form followed by resolution are relatively easy tasks to program for propositional formulas. In the book such programs are given in the Prolog language (of which a short description is given in chapter 8). Extensions to predicate calculus are sketched (in the preface the author says that full source code is available on line at the site of Springer Verlag in UK, but I was unable to find anything). This is quite another matter, not accessible at the undergraduate level: for programs dealing with predicate calculus, one knows that the real problem is their efficiency [1].

The third part contains introductions to three subjects more directly linked to computer science: logic programming, with its adapted resolution scheme (SLD resolution) and variants (concurrent logic programming and constraint logic programming), logic of programs through the deductive system of Hoare, and the Z notations of temporal logic (a matter dear to the author).

The book is broad, dealing with more subjects than is usual at undergraduate level, for example resolution and temporal logic. The book is elementary compared to works such as Basic Proof Theory [2]. But the book is also rigorous. Though there is no miracle making the treatment as complete as in more specialized textbooks [2], the writing is well structured, with precise definitions, propositions and theorems. Each chapter ends with exercises. The wording of these is sometimes shortened in a way that is appropriate for instructors. The author claims that the Springer Verlag Web site in the UK includes answers to these exercises, but I have been unable to reach anything but an error message at the address given.

In conclusion, this is an excellent book.