|
|
 |
|
|
|
|
|
| a book review published in The Bulletin
of Symbolic Logic, Vol.8 No.3 (Sept, 2002) John
Arnold Kalman. John Kalman’s Automated reasoning with Otter is a complete user’s guide for OTTER. William McCune’s OTTER is the most widely used automated theorem-proving program. It is the current offering of the Argonne automated reasoning group led by L. Wos. OTTER and its resolution-based variants are often beaten in the annual CADE theorem-proving contests, but it has the most mathematical results of any prover (although the most famous theorem-prover result, the completeness of Robbins’s axiomatization of Boolean algebras belongs to McCune’s EQP). This book’s author, John Kalman, is noted for solving open problems about equivalential calculus and condensed detachment using OTTER and OTTER’s predecessor ITP. McCune’s OTTER 3.0 reference manual and guide (report ANL-94/6, available through www.mcs.anl.gov/AR/otter) is the best reference manual for OTTER: it is concise and finding information about flags and parameters is easy. For the beginner seeking a theorem-roving overview, Automated reasoning, Introduction and applications by Wos et al. (JSL LI464. LIX1437) is easier reading but it is not specific to OTTER. But Kalman’s book is the best user’s guide (a reference describes what the commands do: a user’s guide shows how to use the commands). It has 705 examples and exercises which cover the needs of beginning and advanced users. It thoroughly covers OTTER’s inference rules (such as binary resolution and hyperresolution, paramodulation), OTTER’s theorem-proving strategies (such as set-of-support and term orderings), OTTER’s many flags and parameters, and the techniques (such as Slolemization) needed to convert a problem in an equiconsistent set of OTTER-readable clauses (universal disjunctive sentences). The CD included with the book contains version 3.04 of the OTTER program and a 3MB Acrobat file with the complete contents of the text. Kalman includes advanced and specialized topics involving Skolem function symbols, term ordering, recursive path orderings, dynamic demodulation, and the many paramodulation flags. He includes topics not found elsewhere such as how to use the passive list to handle inequality and how subsumption can lead to derivational incompleteness. He does not cover fringe features such as Veroff’s linked resolution, hot lists, ancestor subsumption, and conditional demodulation. Kalman’s book is also a fairly comprehensive guide to OTTER’s accomplishments and the type of problems it can solve. About a quarter of the book consists of listings of input and output files for a wide variety of problems OTTER can solve. In areas such as combinatory logic and propositional axiomatizations, OTTER has found publishable results. But for most mathematical problems of medium difficulty ( such as the quadratic formula), OTTER and all other theorem provers usually wander astray in a combinatorial explosion of irrelevancies no matter how the flags and parameter are set. The book’s completeness (no prerequisites are needed) and many exercises make it suitable use as a text on theorem proving. But theorem proving is usually part of an AI course that gives equal time to logic programming, neural nets, and genetic algorithms. At 551 pages and $88, it is too big and expensive for a supplemental reading text. This book has extensive coverage of the logical foundation of theorem proving but usually without proofs. Kalman does not prove J.A. Robinson’s theorem that most general unifiers always exist but he shows how they are generated, why symbol clashes or occurs checks imply non-unifiability, and how to get OTTER to print out most general unifiers. He states but does not prove the many refutational completeness proofs involving resolution, paramodulation, and set of support. The Knuth-Bendix completion procedure is well presented but without the usual theorems about critical pairs, confluence, and termination. Of the texts that cover resolution-based theorem proving with formal proofs, Chang and Lee’s Symbolic logic and mechanical theorem proving (Academic Press, 1973) is the classic. Alexander Leitsch’s The resolution calculus (Springer, 1997) has the most recent references. What proofs there are are done precisely and in full detail – Kleene style. But the mathematics is not elegant. This can be blamed as much on the subject as the author. Automated reasoning does not have the depth, maturity, and beauty of complexity theory. Wos was one of the first to realize that it is primarily an experimental science. Progress depends as much on writing programs to determine what works as on writing papers on what might work. Workers in the field are more impressed with results (such as McCune’s solution of Robbins’s problem) than with theoretical arguments. There are almost no errors. “6,” “7,” “8,” should be “f,” “g,” “h,” on pages 434-435. On page 510 “max-weight” should be “max_weight.” The other errors (pages 116, 363, 377) are harmless. The index is incomplete. It has “paramodulation” but neither “resolution” nor “binary resolution.” It has “substitution” but not “replacement.” On page 82 Kalman abbreviates “inferred-clause-processing procedure” to “icpp.” This will cause problems for a non-linear reader who encounters this un-indexed abbreviation later in the book. The reason for complaining is that while most readers will be advanced OTTER users, the book is far too verbose to be read in its entirely by anyone except beginners. If you need a user’s guide to OTTER that goes beyond McCune’s sixty-page reference manual, this is your only choice.
Dale Myers back to the book Automated Reasoning with OTTER front page
|
