New Book: Proof Theory and Automated Deduction


The following book has recently been published, which may be of
interest to readers of this mailing list.

Proof Theory and Automated Deduction


Jean Goubault-Larrecq
G.I.E. Dyade/INRIA, Rocquencourt, France


Ian Mackie
Ecole Polytechnique, Palaiseau, France

Kluwer Academic Publishers
Volume 6

>From the back cover:

Proof Theory and Automated Deduction is written for final-year
undergraduate and first-year post-graduate students. It should also
serve as a valuable reference for researchers in logic and computer
science. It covers basic notions in logic, with a particular stress on
proof theory, as opposed to, for example, model theory or set theory;
and shows how they are applied in computer science, and especially the
particular field of automated deduction, i.e. the automated search for
proofs of mathematical propositions. We have chosen to give an
in-depth analysis of the basic notions, instead of giving a mere
sufficient analysis of basic and less basic notions. We often derive
the same theorem by different methods, showing how different
mathematical tools can be used to get at the very nature of the
objects at hand, and how these tools relate to each other. Instead of
presenting a linear collection of results, we have tried to show that
all results and methods are tightly interwoven. We believe that
understanding how to travel along this web of relations between
concepts is more important than just learning the basic theorems and
techniques by rote.


List of Figures. Preface. 1. Introduction. 2. Classical Propositional
Logic. 3.  Other Propositional Logics. 4. The Curry-Howard
Correspondence. 5. Modal and Temporal Logics. 6. First-Order Classical
Logic. 7. Resolution. 8. Tableaux, Connections and
Matings. 9. Incorporating Knowledge. 10. Logic Programming
Languages. Appendix A: Answers to Exercises. Appendix B: Basics of
Topology.  Bibliography. Index.

Kluwer Academic Publishers, Dordrecht
ISBN 0-7923-4593-2
April 1997
440 pp.

Ordering information can be found at: