by

Larry Wos and Gail W. Pieper

How can you have your computer reason logically, whether the goal is that of solving a puzzle, designing a circuit, or proving a deep theorem? The answer rests with automated reasoning and a powerful reasoning program called OTTER, currently in use to answer diverse and deep questions in mathematics and logic. This book presents an intriguing and thorough treatment of automated reasoning -- through examples, puzzles, and challenging questions -- and includes a CD-ROM offering OTTER so that you can start your own experimentation immediately. The program is offered for workstations, for the MacIntosh, and for personal computers. To further aid you, the CD-ROM contains numerous input files, proofs, and even copious material now out of print.

No background is needed. If you are a novice, early chapters will lead you gently through the fundamentals of logic and show you how to present problems and questions to an automated reasoning program. On the other hand, even if you are already familiar with automated reasoning, or if you have little interest in computing, this book will intrigue you. In either case, if you enjoy games in which strategy plays a role (as in poker and chess and the like), you will find that reliance on strategy is crucial to OTTER's power and impressive list of successes. Indeed, it offers new and challenging questions, many of which are still unanswered.

Contents:

Foreword by Ross Overbeek

Who should read this book? Ross Overbeek suggests anyone who is "young at heart . . . and interested in understanding automated deduction". Why would one wish to read this book? Overbeek's answer is clear: "You must play with problems if you hope to get insight", and this book offers that opportunity -- from exercises to open questions -- and through your own copy of OTTER found on the included CD-ROM.

Preface

The title of this book (Fascinating Country) suggests the delight that awaits the adventurers who are eager to explore the field of automated reasoning, which is at the frontier of computing. This book is intended as a guide -- to the language, customs, and charms of automated reasoning. The subtitle of the preface (Outrageous Dreams Realized) indicates Wos's enormous satisfaction with the progress automated reasoning has made in the past few decades in answering questions in diverse areas of mathematics and logic.

Chapter 1. The Menu, The Map, and the Magic

To begin one's exploration into this fascinating country, the reader is given a a menu with several problems posed to give a taste of what is to come; a map to guide readers through the various chapters; and a brief introduction to the language (the clause language), the means for drawing conclusions (inference rules), and mechanisms for controlling the program's attack (diverse strategies). Also examined are features distinguishing this "country" from others -- artificial intelligence, for example, and reasoning by persons. The chapter concludes with a glimpse into the next frontier, a future world in which automated reasoning programs have become self-analytical. Will this future program make researchers unnecessary? Not at all!

Chapter 2 - Learning Logic by Example

Since reasoning programs must draw conclusions flawlessly, logic is essential. This chapter provides an introduction to logic -- not the dry, formal approach often found in academia, but an approach based on examples, ranging from "who's married to whom?" to "getting from Gorm to Leadville". Also presented is the language -- called the "clause language" -- used to communicate in this country. Eighteen exercises from ordinary life help ease the culture shock.

Chapter 3 - Automated Reasoning in Full

This chapter is for those who have spent some time in Chapter 2, or those who are already somewhat familiar with the basic elements of logic or automated reasoning. The pace is brisk, as the readers are introduced more fully to relationships in logic, to the use of inference rules and strategies, and to different ways to implement an automated reasoning program on parallel machines. In addition to the twelve exercises, challenges are offered such as: How can one give OTTER the capacity to perform as a set of reasoning programs, or environments, that can function independently?

Chapter 4 - Logic Circuit Design

The basic problem of circuit design is to describe a means to connect the available components in such a way that the overall circuit behaves in the desired way and yet no restrictions are violated. That seems fairly easy, since circuit designers are used to dealing with specifications, and such specifications often can be readily captured in the clause language. The problem is compounded, however, by the fact that more than one way exists to design a circuit -- the fact that the designer is interested in the "best" one: the one using the fewest components or the one being the least expensive or so forth. This chapter shows how an automated reasoning program can provide valuable assistance in circuit design. The discussion covers how to work with functional descriptions, descriptive sentences, or even tables in formulating a circuit design problem for an automated reasoning program. After offering a difficult-to-solve puzzle, the chapter begins with simple circuits and progresses, through a series of five exercises, to advanced techniques in multivalued logic.

Chapter 5 - Logic Circuit Validation

Suppose you have a circuit and wish to know whether the design in fact meets the specifications. This chapter discusses how to analyze a circuit, using demodulation to simplify and canonicalize it, and then how to use an automated reasoning program to compare the results with the specifications. The chapter includes a powerful approach that involves validating subcircuits and then using them in the construction of more complex circuits. For example, once a one-bit adder has been validated, it can be treated as a "black box" -- its internal design ignored, and the same set of demodulators is used to validate a two-bit adder, then a four-bit adder, and so on.

Chapter 6 - Research in Mathematics

In 1997, the world of science was startled by the announcement (in the New York Times) that an automated reasoning program (by the developer of OTTER) had answered a question in mathematics whose answer had eluded some of the finest minds for more than six decades. Without doubt, some of the most startling successes with automated reasoning have been in mathematics. This chapter discusses some of these successes and the strategies offered by OTTER that have been used to find shorter proofs, to answer open questions, and to find models and counterexamples.

Chapter 7 - Research in Formal Logic

Despite the formidable terms - combinatory logic, two-valued sentential logic, equivalential calculus -- you are not required to be an expert in these fields to achieve success. Indeed, recounted here are ways to use the strategies presented earlier, and the automated reasoning program OTTER, to find new axiom systems or new combinators. The chapter concludes with several exercises designed to lead you from manually applying inference rules and strategies to deduce theorems (a labor-intensive and error-prone task) to writing clauses for OTTER to search for shorter derivations. From OTTER's output, you might also develop an appreciation of the beauty and intrigue of logic.

Chapter 8 - The Formal Treatment of Automated Reasoning

For the researcher who delights in knowing the formal foundations of a discipline, this chapter provides what is needed. Complementing the needed definitions, however, are numerous exercises pertinent to the formal material.

Chapter 9 - Wos's Biased Guide for the Effective Use of OTTER

OTTER is a marvelous reasoning assistant. But as with any new colleague, you must learn how to best communicate with OTTER. This chapter suggests ways to speed the learning curve. Some of the suggestions are well documented; others are merely hints -- but hints that are based on considerable experience. Several input files are included to initiate "years and years of enjoyment and success with OTTER".

Chapter 10 - An Author's Appraisal of His Papers

The rather intimidating title of this chapter should in no way deter the reader. Indeed, this chapter, unlike many of the others, presents problems and questions that can be attacked unaided -- without the use of OTTER. Perhaps a better title would be "Vignettes", for featured here are many short sections, each of which corresponds to one of the previously published papers presented in the two-volume book The Collected Works of Larry Wos and found on its included CD-ROM. In addition to presenting an interesting historical perspective of the development of the field of automated reasoning and offering exercises to test your understanding of the material covered in the published papers, these vignettes suggest areas for future research and unsolved problems to be explored.

Chapter 11 - Open Questions, Hard Problems, Intriguing Challenges

If the hard problems presented throughout the book have piqued your interest, this chapter may prove quite entertaining. If you have little or no interest in computing, this chapter may still intrigue you. In particular, presented here are challenging questions and problems organized by area: for example, combinatory logic, ring theory, Boolean algebra, and propositional logic. Here, however, no answers are given, for the answers are not yet known. If you succeed in conquering one of the items, you might well be able to publish the result.

Chapter 12 - Epilogue and After-Dinner Liqueur

The authors could not resist. Instead of simply ending with a summary, this chapter ends with a fascinating puzzle entitled Of Monkey and Men.

Appendixes Featuring Input Files, Proofs, and Output File Fragments

The appendixes are intended to be studied and used in experiments. The input files may prove useful in attacking the deep questions and hard problems offered throughout the book. The given proofs may lead to the discovery of new and better proofs. And the output files give a glimpse of OTTER's approach, a glimpse that may lead to significant breakthroughs.

References

Index

by
Larry Wos and Gail W. Pieper

Automated reasoning programs are successfully tackling challenging problems in mathematics and logic, program verification, and circuit design. This two-volume book includes all the published papers of Larry Wos -- one of the world's pioneers in automated reasoning.

The book has the following special features:

Contents:

Foreword by Robert S. Boyer

In this foreword, Bob Boyer captures the essence of Wos's success: his "passionate ecstasy" in what he considers "both the noblest and most rewarding of human experiences, the development of the power to reason."

Preface

Who are the Significant Seven who influenced, guided, and inspired Wos's research?

Vol. 1 - Exploring the Power of Automated Reasoning includes Wos's papers from 1958 to 1991. Here readers can trace the progress in automated reasoning -- first to solve classroom exercises, then to address more challenging problems, and eventually to answer open questions. Included are formal papers in mathematics and logic journals as well as informal introductions to the field in such journals as Abacus. Here, too, are the first papers published in the Journal of Automated Reasoning, which Wos founded and which continues today.

Vol. 2 - Applying Automated Reasoning to Puzzles, Problems, and Open Questions includes Wos's papers from 1991 to 1999 -- and, yes, he is still publishing here in the year 2000. This volume includes papers introducing new strategies -- such as the kernel strategy, the hot list, and the resonance strategy -- that have enabled Wos and his colleagues to find new combinators, dramatically shorter proofs, and completely new proofs.

Readership: College students, teachers, researchers and historians of computer science.

1639 pages
ISBN: 981-02-4001-5 (set)