A Spectrum of Applications of Automated Reasoning
| dc.creator | Wos, Larry | |
| dc.date | 2002-05-30 | |
| dc.date.accessioned | 2026-07-07T03:18:28Z | |
| dc.date.available | 2026-07-07T03:18:28Z | |
| dc.description | 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. | |
| dc.description | 13 pages | |
| dc.identifier | https://arxiv.org/abs/cs/0205078 | |
| dc.identifier | http://arxiv.org/abs/cs/0205078 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/31126 | |
| dc.subject | Artificial Intelligence | |
| dc.subject | Logic in Computer Science | |
| dc.subject | I.2.3; F.4.1 | |
| dc.title | A Spectrum of Applications of Automated Reasoning | |
| dc.type | text |