Analytic and Non-analytic Proofs
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.
KeywordsInference Rule Proof System Natural Deduction Expansion Term Analytic Proof
Unable to display preview. Download preview PDF.
- 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.Google Scholar
- Wolfgang Bibel. Automatic Theorem Proving. Vieweg. Braunschweig, 1982.Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- J. Herbrand, Logical Writings, Harvard University Press, 1972.Google Scholar
- Dale A. Miller, Proofs in Higher Order Logic, Ph.D. Th., Carnegie-Mellon University, August 1983.Google Scholar
- Dale A. Miller, Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs. 7th Conference on Automated Deduction, Napa, May 1984.Google Scholar
- Frank Pfenning. Conversions between Analytic and Non-analytic Proofs. Tech. Report, Carnegie-Mellon University, 1984. (to appear)Google Scholar