Missing Proofs Found

For close to a century, despite the eorts of ne minds that include Hilbert and Ackermann, Lukasiewicz, and Rose and Rosser, various proofs of a number of signi-cant theorems have remained missing|at least not reported in the literature|amply demonstrating the depth of the corresponding problems. The types of such missing proofs are indeed diverse. For one example, a result may be guaranteed provable be-cause of being valid, and yet no proof has been found. For a second example, a theorem may have been proved via metaargument, but the desired axiomatic proof based solely on the use of a given inference rule may have eluded the experts. For a third example, a theorem may have been announced by a master, but no proof was supplied. The nding of missing proofs of the cited types, as well as of other types, is the focus of this article. The means to nding such proofs rests with heavy use of McCune's automated reasoning program OTTER, reliance on a variety of powerful strategies this program oers, and employment of diverse methodologies. Here we present some of our successes and, because it may prove useful for circuit design and program synthesis as well as in the context of mathematics and logic, detail our approach to nding missing proofs. Well-de ned and unmet challenges are included