A Spectrum of Applications of Automated Reasoning

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 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.