## Abstract

When given a set of properties or conditions (say, three) that are claimed to be equivalent, the claim can be verified by supplying what we call a*circle of proofs*. In the case in point, one proves the second property or condition from the first, the third from the second, and the first from the third. If the proof that 1 implies 2 does not rely on 3, then we say that the proof is pure with respect to 3, or simply say the*proof is pure*. If one can renumber the three properties or conditions in such a way that one can find a circle of three pure proofs — technically, each proof pure with respect to the condition that is neither the hypothesis nor the conclusion — then we say that a*circle of pure proofs* has been found. Here we study the specific question of the existence of a circle of pure proofs for the thirteen shortest single axioms for equivalential calculus, subject to the requirement that condensed detachment be used as the rule of inference. For an indication of the difficulty of answering the question, we note that a single application of condensed detachment to the (shortest single) axiom known as*P*4 (also known as*UM*) with itself yields the (shortest single) axiom*P*5 (also known as*XGF*), and two applications of condensed detachment beginning with*P*5 as hypothesis yields*P*4. Therefore, except for*P*5, one cannot find a pure proof of any of the twelve shortest single axioms when using*P*4 as hypothesis or axiom, for the first application of condensed detachment must focus on two copies of*P*4, which results in the deduction of*P*5, forcing*P*5 to be present in all proofs that use*P*4 as the only axiom. Further, the close proximity in the proof sense of*P*4 when using as the only axiom*P*5 threatens to make impossible the discovery of a circle of pure proofs for the entire set of thirteen shortest single axioms. Perhaps more important than our study of pure proofs, and of a more general nature, we also present the methodology used to answer the cited specific question, a methodology that relies on various strategies and features offered by W. McCune's automated reasoning programOtter. The strategies and features ofOtter we discuss here offer researchers the needed power to answer deep questions and solve difficult problems. We close this article (in the last two sections) with some challenges and some topics for research and (in the Appendix) with a sample input file and some proofs for study.

## Key words

automated reasoning hot list pure proofs strategy## Preview

Unable to display preview. Download preview PDF.

## References

- 1.Kalman, J.: A shortest single axiom for the classical equivalential calculus,
*Notre Dame J. Formal Logic***19**(1978), 141–144.Google Scholar - 2.Kalman, J.: Condensed detachment as a rule of inference,
*Studia Logica***42**(1983), 443–451.Google Scholar - 3.McCharen, J., Overbeek, R. and Wos, L.: Complexity and related enhancements for automated theorem-proving programs,
*Computers and Mathematics with Applications***2**(1976), 1–16.Google Scholar - 4.McCune, W. and Wos, L.: Experiments in automated deduction with condensed detachment, in D. Kapur (ed.),
*Proc. 11th Int. Conf. on Automated Deduction*(CADE-11), Lecture Notes in Artificial Intelligence, 607, Springer-Verlag, New York, 1992, pp. 209–223.Google Scholar - 5.McCune, W.:Otter 3.0, Preprint MCS-P399-1193, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, November 1993.Google Scholar
- 6.Peterson, J.: Shortest single axioms for the equivalential calculus,
*Notre Dame J. Formal Logic***17**(1976), 267–271.Google Scholar - 7.Wos, L., Winker, S., Veroff, R., Smith, B., and Henschen, L.: Questions concerning possible shortest single axioms in equivalential calculus: An application of automated theorem proving to infinite domains,
*Notre Dame J. Formal Logic***24**(1983) 205–223.Google Scholar - 8.Wos, L., Winker, S., Veroff, R., Smith, B., and Henschen, L.: A new use of an automated reasoning assistant: Open questions in equivalential calculus and the study of infinite domains,
*Artificial Intelligence***22**(1984), 303–356.Google Scholar - 9.Wos, L.:
*Automated Reasoning: 33 Basic Research Problems*, Prentice-Hall, Englewood Cliffs, NJ, 1987.Google Scholar - 10.Wos, L.: Meeting the challenge of fifty years of logic,
*J. Automated Reasoning***6**(2) (1990), 213–222.Google Scholar - 11.Wos, L., Overbeek, R., Lusk, E., and Boyle, J.:
*Automated Reasoning: Introduction and Applications*, 2nd edn, McGraw-Hill, New York, 1992.Google Scholar - 12.Wos, L.: Personal information, Argonne National Laboratory, 1994.Google Scholar
- 13.Wos, L.:
*Automating the Search for Elegant Proofs: An Experimenter's Notebook*. Academic Press, San Diego, CA, 1995 (to appear).Google Scholar