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 acircle 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 theproof 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 acircle 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 asP4 (also known asUM) with itself yields the (shortest single) axiomP5 (also known asXGF), and two applications of condensed detachment beginning withP5 as hypothesis yieldsP4. Therefore, except forP5, one cannot find a pure proof of any of the twelve shortest single axioms when usingP4 as hypothesis or axiom, for the first application of condensed detachment must focus on two copies ofP4, which results in the deduction ofP5, forcingP5 to be present in all proofs that useP4 as the only axiom. Further, the close proximity in the proof sense ofP4 when using as the only axiomP5 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 wordsautomated reasoning hot list pure proofs strategy
Unable to display preview. Download preview PDF.
- 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