Finding missing proofs with automated reasoning

Studia Logica 68 (3):329-356 (2001)
This article features long-sought proofs with intriguing properties (such as the absence of double negation and the avoidance of lemmas that appeared to be indispensable), and it features the automated methods for finding them. The theorems of concern are taken from various areas of logic that include two-valued sentential (or propositional) calculus and infinite-valued sentential calculus. Many of the proofs (in effect) answer questions that had remained open for decades, questions focusing on axiomatic proofs. The approaches we take are of added interest in that all rely heavily on the use of a single program that offers logical reasoning, William McCune's automated reasoning program OTTER. The nature of the successes and approaches suggests that this program offers researchers a valuable automated assistant. This article has three main components. First, in view of the interdisciplinary nature of the audience, we discuss the means for using the program in question (OTTER), which flags, parameters, and lists have which effects, and how the proofs it finds are easily read. Second, because of the variety of proofs that we have found and their significance, we discuss them in a manner that permits comparison with the literature. Among those proofs, we offer a proof shorter than that given by Meredith and Prior in their treatment of ukasiewicz's shortest single axiom for the implicational fragment of two-valued sentential calculus, and we offer a proof for the ukasiewicz 23-letter single axiom for the full calculus. Third, with the intent of producing a fruitful dialogue, we pose questions concerning the properties of proofs and, even more pressing, invite questions similar to those this article answers.
Keywords Philosophy   Logic   Mathematical Logic and Foundations   Computational Linguistics
Categories (categorize this paper)
Reprint years 2004
DOI 10.1023/A:1012486904520
 Save to my reading list
Follow the author(s)
My bibliography
Export citation
Find it on Scholar
Edit this record
Mark as duplicate
Revision history
Request removal from index
Download options
Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 27,208
Through your library
References found in this work BETA

No references found.

Add more references

Citations of this work BETA

Add more citations

Similar books and articles

Monthly downloads

Added to index


Total downloads

22 ( #226,207 of 2,164,289 )

Recent downloads (6 months)

2 ( #188,554 of 2,164,289 )

How can I increase my downloads?

My notes
Sign in to use this feature

There  are no threads in this forum
Nothing in this forum yet.

Other forums