Abstract
This paper contains the results of experiments with several search strategies on 112 problems involving condensed detachment. The problems are taken from nine different logic calculi: three versions of the two-valued sentential calculus, the many-valued sentential calculus, the implicational calculus, the equivalential calculus, the R calculus, the left group calculus, and the right group calculus. Each problem was given to the theorem prover Otter and was run with at least three strategies: (1) a basic strategy, (2) a strategy with a more refined method for selecting clauses on which to focus, and (3) a strategy that uses the refined selection mechanism and deletes deduced formulas according to some simple rules. Two new features of Otter are also presented: the refined method for selecting the next formula on which to focus, and a method for controlling memory usage.
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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
A. Church. Introduction to Mathematical Logic, volume I. Princeton University Press, 1956.
J. A. Kalman. Axiomatizations of logics with values in groups. Journal of the London Math. Society, 2(14):193–199, 1975.
J. A. Kalman. Computer studies of T→-W-I. Relevance Logic Newsletter, 1:181–188, 1976.
J. A. Kalman. A shortest single axiom for the classical equivalential calculus. Notre Dame Journal of Formal Logic, 19:141–144, 1978.
J. A. Kalman. Condensed detachment as a rule of inference. Studia Logica, LXII(4):443–451, 1983.
E. J. Lemmon, C. A. Meredith, D. Meredith, A. N. Prior, and I. Thomas. Calculi of pure strict implication. Technical report, Canterbury University College, Christchurch, 1957. Reprinted in Philosophical Logic, Reidel, 1970.
J. Łukasiewicz. Elements of Mathematical Logic. Pergamon Press, 1963. English translation of the second edition (1958) of Elementy logiki matematycznej, PWN, Warsaw.
J. Łukasiewicz. Selected Works. North-Holland, 1970. Edited by L. Borkowski.
W. McCune. Otter 2.0 Users Guide. Tech. Report ANL-90/9, Argonne National Laboratory, Argonne, IL, March 1990.
W. McCune. Automated discovery of new axiomatizations of the left group and right group calculi. Preprint MCS-P220-0391, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, 1991.
W. McCune. Single axioms for the left group and right group calculi. Preprint MCS-P219-0391, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, 1991.
C. A. Meredith. Single axioms for the systems (C,N), (C,0), and (A,N) of the two-valued propositional calculus. Journal of Computing Systems, 1:155–164, 1953.
C. A. Meredith and A. N. Prior. Equational logic. Notre Dame Journal of Formal Logic, 9:212–226, 1968.
D. Meredith. In memoriam Carew Arthur Meredith (1904–1976). Notre Dame Journal of Formal Logic, 18:513–516, 1977.
J. G. Peterson. Shortest single axioms for the classical equivalential calculus. Notre Dame Journal of Formal Logic, 17(2):267–271, 1976.
J. G. Peterson. The possible shortest single axioms for EC-tautologies. Report 105, Dept. of Mathematics, University of Auckland, 1977.
F. Pfenning. Single axioms in the implicational propositional calculus. In E. Lusk and R. Overbeek, editors, Proceedings of the 9th International Conference on Automated Deduction, Lecture Notes in Computer Science, Vol. 310, pages 710–713, New York, 1988. Springer-Verlag.
L. Wos. Meeting the challenge of fifty years of logic. Journal of Automated Reasoning, 6(2):213–232, 1990.
L. Wos. Automated reasoning and Bledsoe's dream for the field. In R. S. Boyer, editor, Automated Reasoning: Essays in Honor of Woody Bledsoe, chapter 15, pages 297–342. Kluwer Academic Publishers, 1991.
L. Wos and W. McCune. The application of automated reasoning to proof translation and to finding proofs with specified properties: A case study in many-valued sentential calculus. Tech. Report ANL-91/19, Argonne National Laboratory, Argonne, IL, 1991. In preparation.
L. Wos, S. Winker, W. McCune, R. Overbeek, E. Lusk, R. Stevens, and R. Butler. Automated reasoning contributes to mathematics and logic. In M. Stickel, editor, Proceedings of the 10th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Vol. 449, pages 485–499, New York, July 1990. Springer-Verlag.
L. Wos, S. Winker, B. Smith, R. Veroff, and L. Henschen. A new use of an automated reasoning assistant: Open questions in equivalential calculus and the study of infinite domains. Artificial Intelligence, 22:303–356, 1984.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
McCune, W., Wos, L. (1992). Experiments in automated deduction with condensed detachment. In: Kapur, D. (eds) Automated Deduction—CADE-11. CADE 1992. Lecture Notes in Computer Science, vol 607. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55602-8_167
Download citation
DOI: https://doi.org/10.1007/3-540-55602-8_167
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55602-2
Online ISBN: 978-3-540-47252-0
eBook Packages: Springer Book Archive