| |
|
 |
|
 |
552 pages 10x7 inches w/ CDROM
Feb 2001 Hardcover
ISBN 1-58949-004-5
US$88 |
|
|
|
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.
|
|
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.
|
|
|
|