This is a slighty revised version of the 1985 edition of my logic book. Many ty-
pos and errors have been corrected and the line drawings have been improved.
Most mistakes were minor, except for a subtle error in Theorem 4.3.3. Indeed,
the second part of the theorem about the complexity of the proof tree T ob-
tained from a resolution refutation D is false: It is not necessarily the case
that the number of leaves of T is less than or equal to the number of resolution
steps in D. As a consequence, Lemma 4.3.4 is also false.