Argonne National Laboratory

Axiomatic Proofs through Automated Reasoning

TitleAxiomatic Proofs through Automated Reasoning
Publication TypeReport
Year of Publication2000
AuthorsFitelson, B, Wos, L
Series TitleBulletin of the Section of Logic
Date Published05/2000
Other NumbersANL/MCS-P827-0500

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