552 pages 10x7 inches w/ CDROM
Feb 2001 Hardcover
ISBN 1-58949-004-5


    Buy It

Automating reasoning has been described as ``one of the most exciting and potentially fruitful areas of research that there has ever been.'' This book provides you with the means: a powerful reasoning program called Otter, currently in use to answer diverse and deep questions in mathematics and logic. The volume presents an intriguing and thorough treatment of automated reasoning and Otter -- through numerous examples, exercises, and challenging questions. No background is needed. The early chapters lead you through Otter's fundamental operations and show you how to present questions and problems to Otter, beginning with simple puzzles. Numerous input files and proofs are provided, so you can experiment and play with problems. Gradually, more challenging applications are introduced, and more powerful strategies discussed -- strategies that are crucial to Otter's power and impressive list of successes.


The full text of a book review by D Myers
in The Bulletin of Symbolic Logic, Vol.8 No.3 (Sept 2002)

"Kalman's book is a masterpiece. The book contains a unique blend of theoretical and experimental material. Its myriad of worked examples make it a joy to use in the classroom. Students, teachers, and researchers alike should benefit greatly from Kalman's expertise." 
  -- Branden Fitelson (University of Wisconsin)


Chs. 1-5 give an introduction to logic, automated reasoning, and Otter. The approach is based on examples, including "the wolf, the goat, and the cabbages", and includes numerous exercises that lead you gently from the simple to the complex. Included in these chapters is a discussion of the language for conveying a problem to Otter, the means for drawing conclusions, and mechanisms for controlling the program's attack.
Chs. 6-9 provide a fuller treatment of such concepts as substitution, hyperresolution, and proof by contradiction. These chapters are for readers who have "some acquaintance" with first-order logic. The fine detail is complemented nicely by illustrations and case studies,  as well as cryptarithmetic puzzles and puzzles on "truth-tellers and liars" and "knights and knaves" -- all of which can be translated into clauses and solved by running Otter.

Ch. 10 shows how, with the help of more sophisticated techniques, the class of reasoning problems that Otter can attack can be greatly extended. In particular, this chapter focuses on propositional connectives such as "not", "or", and "and", and discusses the notion of "logical equivalence." The chapter ends with a helpful section on how Otter can be used to translate formulas into clause automatically.
The remaining chapters are concerned mainly with logical problems whose solution requires reasoning about equality. One simple example is the following: Suppose we know that (a) if two persons x and y are acquainted, then x is also acquainted with y's spouse, and (b) Dick's spouse is acquainted with Eve's spouse.   The problem is to show that (c) Dick is acquainted with Eve.  Implicit in this problem is the idea that (d) if x and y are acquainted, then y and x are acquainted, and (e) the spouse of the spouse of x is x. To use the hypothesis (e), reasoning about equality is needed. Otter provides special facilities for investigating such problems.

Larry Wos (Argonne Nantional Lab), pioneer in the field of automated reasoning, states emphatically in the Foreword: "A virtually limitless amount of treasure awaits the person who masters the use of Otter." That treasure includes the enjoyment of solving puzzles, the satisfaction of finding a shorter proof, the delight in answering a previously open question. "And even moderate familiarity with the program," claims Wos, "can yield information that has eluded great minds for decades."


Otter has answered more open questions, found better proofs, and solved deeper problems than any other reasoning program known. And, Otter is readily available on the Web, from its developer William McCune here.


John Kalman, received his Ph.D. from Harvard University in 1955 with Professor G.W. Mackey as Thesis Director, is a professor emeritus at the University of Auckland, New Zealand. He has written more than 25 articles on logic, as well as on mathematics, algebra, and automated deduction. Kalman's work on computer-aided studies of shortest single axioms for classical equivalential calculus was published in the Notre Dame Journal of Formal Logic in 1978 -- the earliest occasion that a renowned journal devoted to logic published a paper in which automated reasoning played the key role. His research spawned numerous papers on the topic. In particular, his visit to Argonne National Laboratory in 1979  began a decade of collaboration that resulted in the answering of several open questions in equivalential calculus. Kalman also was one of the earliest and heaviest users of ITP, an automated reasoning program developed at Argonne and the predecessor of the current Otter.