Abstract
In automated theorem Poving different kinds of proof systems have been used. Traditional proof systems, such as Hilbert-style proofs or natural deduction we call non-analytic, while resolution or mating proof systems we call analytic. There are many good reasons to study the connections between analytic and non-analytic proofs. We would like a theorem prover to make efficient use of both analytic and non-analytic methods to get the best of both worlds.
In this paper we present an algorithm for translating from a particular non-anMytic proof system to analytic proofs. Moreover, some results about the translation in the other direction are refornmlated and known algorithms improved, hnplementation of the algorithms presented for use in research and teaching logic is under way at Carnegie-Mellon University in the framework of TPS and its educational counterpart ETPS.
Finally we show how to obtain non-analytic proofs from resolution refutations. As an application, resolution refutations can be translated into comprehensible natural deduction proofs.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Peter B. Andrews, Refutations by Matings, IEEE Transactions on Computers C-25 (1976), 801–807.
Peter B. Andrews, Transforming Matings into Natural Deduction Proofs. in 5th Conference on Automated Deduction, Les Arcs. France. edited by W. Bibel and R. Kowalski. Lecture Notes in Computer Science 87. Springer-Verlag. 1980, 281–292.
Peter B. Andrews. Theorem Proving via General Matings. Journal of the Association for Computing Machinery 28 (1981), 193–214.
Wolfgang Bibel. Automatic Theorem Proving. Vieweg. Braunschweig, 1982.
W. Bibel and J. Schreiber, Proof search in a Gentzen-like system of first-order logic. Proceedings of the International Computing Symposium, 1975. pp. 205–212.
W. W. Bledsoe, Non-resolution Theorem Proving, Artificial Intelligence 9 (1977), 1–35.
G. Gentzen, Investigations into Logical Deductions. In The Collected Papers of Gerhard Gentzen, M. E. Szabo, Ed.,North-Holland Publishing Co., Amsterdam, 1969, pp. 68–131.
J. Herbrand, Logical Writings, Harvard University Press, 1972.
Dale A. Miller, Proofs in Higher Order Logic, Ph.D. Th., Carnegie-Mellon University, August 1983.
Dale A. Miller, Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs. 7th Conference on Automated Deduction, Napa, May 1984.
Frank Pfenning. Conversions between Analytic and Non-analytic Proofs. Tech. Report, Carnegie-Mellon University, 1984. (to appear)
J.A. Robinson, A machine-oriented logic based on the resolution principle, Journal of the Association for Computing Machinery 12 (1965), 23–41.
R. M. Smullyan, First-Order Logic, Springer-Verlag, Berlin, 1968.
R. Statman, Lower Bounds on Herbrand’s Theorem, Proceedings of the American Mathematical Society 75 (1979), 104–107.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1984 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pfenning, F. (1984). Analytic and Non-analytic Proofs. In: Shostak, R.E. (eds) 7th International Conference on Automated Deduction. CADE 1984. Lecture Notes in Computer Science, vol 170. Springer, New York, NY. https://doi.org/10.1007/978-0-387-34768-4_23
Download citation
DOI: https://doi.org/10.1007/978-0-387-34768-4_23
Publisher Name: Springer, New York, NY
Print ISBN: 978-0-387-96022-7
Online ISBN: 978-0-387-34768-4
eBook Packages: Springer Book Archive