A Spectrum of Applications of Automated Reasoning
Larry Wos

TL;DR
This paper reviews the diverse applications of automated reasoning, especially using OTTER, in solving open problems, optimizing proofs, and exploring axiomatic systems, highlighting strategies and open challenges.
Contribution
It provides a comprehensive overview of how OTTER can be applied across various logical and mathematical problems, emphasizing new methodologies for proof optimization and problem solving.
Findings
OTTER successfully answered open questions and discovered new axioms.
Strategies for proof shortening and simplification are effective.
Automated reasoning can provide new insights into proof structures.
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Logic, programming, and type systems · Semantic Web and Ontologies
