The consideration of careful reasoning can be traced to Aristotle and earlier authors. The possibility of rigorous rules for drawing conclusions can certainly be traced to the Middle Ages when types o f syllogism were studied. Shortly after the introduction of computers, the audacious scientist naturally envisioned the automation of sound reasoning—reasoning in which conclusions that are drawn follow l ogically and inevitably from the given hypotheses. Did the idea spring from the intent to emulate s Sherlock Holmes and Mr. (...) Spock (of Star Trek) in ﬁction and Hilbert and Tarski and other great mind i n nonﬁction? Each of them applied logical reasoning to answer questions, solve problems, and ﬁnd e proofs. But can such logical reasoning be fully automated? Can a single computer program b d esigned to offer sufﬁcient power in the cited contexts? Indeed, while the use of computers was quickly accepted for numerical calculations and data processing, intense skepticism persisted—even in the early 1960s—regarding the ability of computers to a pply effective reasoning. The following simple (but perhaps deceptive) example provides a taste of the type of argument that might have been used to support this skepticism. (shrink)
detail a question that, for a quarter of a century, remained open despite intense study by various researchers. Is the formula XC B = e(x e(e(e( ) e( )) z)) a single axiom for the classical equivalential calculus when the rules of inference consist..
This article answers two questions (posed in the literature), each concerning the guaranteed existence of proofs free of double negation. A proof is free of double negation if none of its deduced steps contains a term of the formn(n(t)) for some term t, where n denotes negation. The first question asks for conditions on the hypotheses that, if satisfied, guarantee the existence of a double-negation-free proof when the conclusion is free of double negation. The second question asks about the existence (...) of an axiom system for classical propositional calculus whose use, for theorems with a conclusion free of double negation, guarantees the existence of a double-negation-free proof. After giving conditions that answer the first question, we answer the second question by focusing on the Lukasiewicz three-axiom system. We then extend our studies to infinite-valued sentential calculus and to intuitionistic logic and generalize the notion of being double-negation free. The double-negation proofs of interest rely exclusively on the inference rule condensed detachment, a rule that combines modus ponens with an appropriately general rule of substitution. The automated reasoning program Otter played an indispensable role in this study. (shrink)
Shortest possible axiomatizations for the implicational fragments of the modal logics S4 and S5 are reported. Among these axiomatizations is included a shortest single axiom for implicational S4—which to our knowledge is the ﬁrst reported single axiom for that system—and several new shortest single axioms for implicational S5. A variety of automated reasoning strategies were essential to our discoveries.
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. (shrink)