MILESTONES FOR AUTOMATED REASONING WITH OTTER
Abstract
In the beginning (the early 1960s), the long-term goal of automated reasoning (although the field at the time was not known by that name) was the design and implementation of a program whose use would lead to "real" and significant contributions to mathematics by offering sufficient power for the discovery of proofs. The realization of that goal appeared to be at least six decades in the future. However, with amazement and satisfaction, we can report that fewer than four decades were required. In this article, we present evidence for this claim, thanks to W. McCune's program OTTER. Our focus is on various landmarks, or milestones, of two types. One type concerns the formulation of new strategies and methodologies whose use greatly enhances the power of a reasoning program. A second type focuses on actual contributions to mathematics and (although not initially envisioned) to logic. We give examples of each type of milestone, and, perhaps of equal importance, demonstrate that advances are far more likely to occur if the two classes are closely intertwined. We draw heavily on material presented in great detail in the new book Automated Reasoning and the Discovery of Missing and Elegant Proofs, published by Rinton Press.
The submitted manuscript has been created by the University of Chicago as Operator of Argonne National Laboratory ("Argonne") under Contract No. W-31-109-ENG-38 with the U.S. Department of Energy. The U.S. Government retains for itself, and others acting on its behalf, a paid-up, nonexclusive, irrevocable worldwide license in said article to reproduce, prepare derivative works, distribute copies to the public, and perform publicly and display publicly, by or on behalf of the Government.
| Remember to check out the Most Cited Articles! |
|---|
|
Check out Notable Titles in Artificial Intelligence. |
