A spectrum of applications of automated reasoning [electronic resource].
- Washington, D.C. : United States. Dept. of Energy, 2002.
Oak Ridge, Tenn. : Distributed by the Office of Scientific and Technical Information, U.S. Dept. of Energy.
- Physical Description:
- 13 pages : digital, PDF file
- Additional Creators:
- Argonne National Laboratory
United States. Department of Energy
United States. Department of Energy. Office of Scientific and Technical Information
- The likelihood of an automated reasoning program being of substantial assistance for a wide spectrum of applications rests with the nature of the options and parameters it offers on which to base needed strategies and methodologies. This article focuses on such a spectrum, featuring W. McCune's program OTTER, discussing widely varied successes in answering open questions, and touching on some of the strategies and methodologies that played a key role. The applications include finding a first proof, discovering single axioms, locating improved axiom systems, and simplifying existing proofs. The last application is directly pertinent to the recently found (by R. Thiele) Hilbert's twenty-fourth problem--which is extremely amenable to attack with the appropriate automated reasoning program, a problem concerned with proof simplification. The methodologies include those for seeking shorter proofs and for finding proofs that avoid unwanted lemmas or classes of term, a specific option for seeking proofs with smaller equational or formula complexity, and a different option to address the variable richness of a proof. The type of proof one obtains with the use of OTTER is Hilbert-style axiomatic, including details that permit one sometimes to gain new insights. We include questions still open and challenges that merit consideration.
- Published through SciTech Connect.
2002 AMS and MAA Spring Southeastern Section Meeting, Atlanta, GA (US), 03/08/2002--03/10/2002.
- Funding Information:
View MARC record | catkey: 14346751