文档介绍：Logic puter Science
Foundations of
Automatic Theorem Proving
Copyright 2003, Jean H. Gallier
June 2003
Jean Gallier
University of Pennsylvania
Department puter and Information Science
200 South 33rd Street
Philadelphia, Pa 19104
USA
e-mail: ******@
To Anne, my wife,
Mia, Philippe and Sylvie, my children,
and my mother, Simone
Preface (2003 Edition)
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 . Indeed,
the second part of the theorem about plexity 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 is also false.
In this revised edition, we simply removed all statements about -
plexity of the conversion of resolution refutations into proof trees. Hopefully,
this part of the book is now correct, as well as the rest of it!
Some parts of the book have now aged, in particular, the parts about
PROLOG. Also, eighteen years later, I would prefer to present some of the
material in a different order and in a different manner. In particular, I would
separate more clearly the material on the resolution method (Chapter 4) from
the more proof-theory oriented material. However, I consider this too big a
task and this mildly revised version will have to do (at least, for now!).
Ideally, a number of topics should also be covered, for example, some
basics of constructive logic, linear logic, temporal logic and model checking.
Again, this is too formidable a task for a single individual and I hope that
readers enjoy this new version of my book anyway.
It should be noted that this book is of “preTEX vintage.” This means
that LaTEX was not available at the time this book was w