In writing this book, our goal was to produce a text suitable for a
first course in mathematical logic more attuned than the traditional
textbooks to the re- cent dramatic growth in the applications oflogic to
computer science. Thus, our choice oftopics has been heavily influenced
by such applications. Of course, we cover the basic traditional topics:
syntax, semantics, soundnes5, completeness and compactness as well as a
few more advanced results such as the theorems of Skolem-Lowenheim and
Herbrand. Much ofour book, however, deals with other less traditional
topics. Resolution theorem proving plays a major role in our treatment
of logic especially in its application to Logic Programming and PRO-
LOG. We deal extensively with the mathematical foundations ofall three
ofthese subjects. In addition, we include two chapters on nonclassical
logics - modal and intuitionistic - that are becoming increasingly
important in computer sci- ence. We develop the basic material on the
syntax and semantics (via Kripke frames) for each of these logics. In
both cases, our approach to formal proofs, soundness and completeness
uses modifications of the same tableau method in- troduced for classical
logic. We indicate how it can easily be adapted to various other special
types of modal logics. A number of more advanced topics (includ- ing
nonmonotonic logic) are also briefly introduced both in the nonclassical
logic chapters and in the material on Logic Programming and PROLOG.