AXIOMATIC PROOFS THROUGH AUTOMATED REASONING
Branden Fitelson, Larry Wos · 2000
A search of the seminal papers and significant books devoted to the study of various types of logic reveals that many proofs are missing. Indeed, if one seeks an axiomatic proof (of the type that Hilbert enjoyed) relying solely on, say, condensed detachment, in many cases one finds that none is offered by the literature. In part prompted by this discovery, we embarked on an intense study designed to find the missing proofs. In this article, we list many of our successes and discuss the methodologies used to obtain them. We also show how OTTER has proved valuable in finding proofs that avoid both the use of perhaps-thought-to-be indispensable lemmas and the use of an unexpected class of terms. Because crucial to our attack was the use of the automated reasoning program OTTER, we include an intuitive introduction to the subject. OTTER may well prove useful as an assistant in the research of others. 1. Nature, Incentive, and Perspective Papers in logic and in mathematics abound with lists of lemmas, corollaries, and theorems, none, some, or all of which are accompanied by a proof. The nature and type of proof vary widely. At one end of the spectrum, in both logic and mathematics, one finds proofs based on induction, on the use of Zorn’s lemma, or on some other type of metaargument. At the other end of the spectrum, (as preferred