OTTER and the Moufang identity problem

This article provides additional evidence of the value of using an automated reasoning program as a research assistant. Featured is the use of Bill McCune's program OTTER to find proofs of theorems taken from the study of Moufang loops, but not just any proofs. Specifically, the proofs satisfy the property of purity. In particular, when given, say, four equivalent identities (which is the case in this article), one is asked to prove the second identity from the first, the third from the second, the fourth from the third, and the first from the fourth. If the proof that 1 implies 2 does not rely on 3 or 4, then by definition the proof is pure with respect to 3 and 4, or simply the proof is pure. If for the four identities one finds four pure proofs showing that 1 implies 2, 2 implies 3, 3 implies 4, and 4 implies 1, then by definition one has found a circle of pure proofs. By finding the needed twelve pure proofs, this article shows that there does exist a circle of pure proofs for the four equivalent identities for Moufang loops and for all orderings of the identities; however, for much of this article, the emphasis is on the first three identities. In addition — in part to promote the use of automated reasoning programs and to answer questions concerning the choice of options — featured here is the methodology that was employed and a discussion of some of the obstacles, some of which are subtle. The approach relies on paramodulation (which generalizes equality substitution), on demodulation, and — so crucial for attacking deep questions and hard problems — on various strategies, most important of which are the hot list strategy, the set of support strategy, and McCune's ratio strategy. To permit verification of the results presented here, extension of them, and application of the methodology to other unrelated fields, a sample input file and four proofs (relevant to a circle of pure proofs for the four identities) are included. Research topics and challenges are offered at the close of this article.This work was supported by the Mathematical, Information, and Computational Sciences Division subprogram of the Office of Computational and Technology Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

Vanquishing the XCB Question: The Methodological Discovery of the Last Shortest Single Axiom for the Equivalential Calculus

With the inclusion of an effective methodology, this article answers in detail a question that, for a quarter of a century, remained open despite intense study by various researchers. Is the formula XCB=e(x,e(e(e(x,y),e(z,y)),z)) a single axiom for the classical equivalential calculus when the rules of inference consist of detachment (modus ponens) and substitution Where the function e represents equivalence, this calculus can be axiomatized quite naturally with the formulas e(x,x), e(e(x,y),e(y,x)), and e(e(x,y),e(e(y,z),e(x,z))), which correspond to reflexivity, symmetry, and transitivity, respectively. (We note that e(x,x) is dependent on the other two axioms.) Heretofore, thirteen shortest single axioms for classical equivalence of length eleven had been discovered, and XCB was the only remaining formula of that length whose status was undetermined. To show that XCB is indeed such a single axiom, we focus on the rule of condensed detachment, a rule that captures detachment together with an appropriately general, but restricted, form of substitution. The proof we present in this paper consists of twenty-five applications of condensed detachment, completing with the deduction of transitivity followed by a deduction of symmetry. We also discuss some factors that may explain in part why XCB resisted relinquishing its treasure for so long. Our approach relied on diverse strategies applied by the automated reasoning program OTTER. Thus ends the search for shortest single axioms for the equivalential calculus.     

On Computer-Assisted Proofs in Ordinal Number Theory

Some basic theorems about ordinal numbers were proved using McCunes computer program OTTER, building on Quaifes modification of Gödels class theory. Our theorems are based on Isbells elegant definition of ordinals. Neither the axiom of regularity nor the axiom of choice is used.     

The semantics of answer literals

We describe a semantics for answer literals that is not tied to the specific detaisl of the resolution proof procedure. We also describe a number of applications of answer literals to mathematical theorem proving.Author supported by NSF Grant CCR-9503445.     

Computer Proofs in Gödel’s Class Theory with Equational Definitions for Composite and Cross

Some basic theorems about composition and other key constructs of set theory were proved using McCunes computer program OTTER, building on Quaifes modification of Gödels class theory. Our proofs use equational definitions in terms of Gödels flip and rotate functors. A new way to prove the composition of homomorphisms theorem is also presented.     

Single axioms for groups and Abelian groups with various operations

This paper summarizes the results of an investigation into single axioms for groups, both ordinary and Abelian, with each of following six sets of operations: {product, inverse}, {division}, {double division, identity}, {double division, inverse}, {division, identity}, and {division, inverse}. In all but two of the twelve corresponding theories, we present either the first single axioms known to us or single axioms shorter than those previously known to us. The automated theorem-proving program OTTER was used extensively to construct sets of candidate axioms and to search for and find proofs that given candidate axioms are in fact single axioms.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

The Hot List Strategy

Experimentation strongly suggests that, for attacking deep questions and hard problems with the assistance of an automated reasoning program, the more effective paradigms rely on the retention of deduced information. A significant obstacle ordinarily presented by such a paradigm is the deduction and retention of one or more needed conclusions whose complexity sharply delays their consideration. To mitigate the severity of the cited obstacle, I formulated and feature in this article the hot list strategy. The hot list strategy asks the researcher to choose, usually from among the input statements characterizing the problem under study, one or more statements that are conjectured to play a key role for assignment completion. The chosen statements – conjectured to merit revisiting, again and again – are placed in an input list of statements, called the hot list. When an automated reasoning program has decided to retain a new conclusion C – before any other statement is chosen to initiate conclusion drawing – the presence of a nonempty hot list (with an appropriate assignment of the input parameter known as heat) causes each inference rule in use to be applied to C together with the appropriate number of members of the hot list. Members of the hot list are used to complete applications of inference rules and not to initiate applications. The use of the hot list strategy thus enables an automated reasoning program to briefly consider a newly retained conclusion whose complexity would otherwise prevent its use for perhaps many CPU-hours. To give evidence of the value of the strategy, I focus on four contexts: (1) dramatically reducing the CPU time required to reach a desired goal, (2) finding a proof of a theorem that had previously resisted all but the more inventive automated attempts, (3) discovering a proof that is more elegant than previously known, and (4) answering a question that had steadfastly eluded researchers relying on an automated reasoning program. I also discuss a related strategy, the dynamic hot list strategy (formulated by my colleague W. McCune), that enables the program during a run to augment the contents of the hot list. In the Appendix, I give useful input files and interesting proofs. Because of frequent requests to do so, I include challenge problems to consider, commentary on my approach to experimentation and research, and suggestions to guide one in the use of McCunes automated reasoning program OTTER.     

OTTER experiments in a system of combinatory logic

This paper describes some experiments involving the automated theorem-proving program OTTER in the system TRC of illative combinatory logic. We show how OTTER can be steered to find a contradiction in an inconsistent variant of TRC, and present some experimentally discovered identities in TRC.This work was supported by the Office of Scientific Computing U.S. Department of Energy, under the Summer 1994 Faculty Research Participation Program at Argonne National Laboratory.