Book review

This book is the 2nd volume of Automated Reasoning Series (William Pase ed.; first volume of this series was appeared at Kluwer in 1991, edited by R.S. Boyer, with the title Automated Reasoning; Essays in Honor of Woody Bledsoe). As author said, the book is the revised version of his Ph.D. dissertation; the proofs presented are done by theorem provers ITP and OTTER (especially). It's main goal is to describe various applications of automated reasoning in pure mathematics.

The structure of the book is: preface, six chapters, three appendices, a list of references, name and subject indexes.

The preface shows author's view of automated reasoning research. First chapter contains an introduction to automated reasoning; the next five chapters refer to: Von Neumann-Bernays-Gödel (NGB) set theory (a new clausal version of NGB set theory; over 400 theorems proved semiautomatically using OTTER); Peano's arithmetic (more than 1200 definitions and theorems in elementary number theory); Tarski's geometry (a complete first-order axiomatization of Euclidean plane geometry within OTTER); Löb's theorem and Gödel's two incompleteness theorems (formalism of modal logic calculus K4; very high level automated proofs of Löb's and Gödel's theorems); unsolved problems in elementary number theory (31 such problems viewed as challenges for reasoning systems).

The three above-mentioned appendices contain: Gödel's axioms for set theory; Theorems proved in NGB set theory; Theorems proved in Peano's arithmetic.

The book is very pleasantly written and the typesetting is performed in excellent conditions. Although its price is high enough, I consider that this book can assist researchers in pure mathematics (set theory, number theory, axiomatic geometry, mathematical logic), computer science (logic programming, expert systems, program verification, real-time system control, logic circuit design and validation, control of intelligent robots), and last year students working in this fascinating field of automatic reasoning.