Analytic and Non-analytic Proofs

  • Frank Pfenning
Part of the Lecture Notes in Computer Science book series (LNCS, volume 170)


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.


Inference Rule Proof System Natural Deduction Expansion Term Analytic Proof 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Peter B. Andrews, Refutations by Matings, IEEE Transactions on Computers C-25 (1976), 801–807.MathSciNetCrossRefzbMATHGoogle Scholar
  2. [2]
    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
  3. [3]
    Peter B. Andrews. Theorem Proving via General Matings. Journal of the Association for Computing Machinery 28 (1981), 193–214.MathSciNetCrossRefzbMATHGoogle Scholar
  4. [4]
    Wolfgang Bibel. Automatic Theorem Proving. Vieweg. Braunschweig, 1982.Google Scholar
  5. [5]
    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
  6. [6]
    W. W. Bledsoe, Non-resolution Theorem Proving, Artificial Intelligence 9 (1977), 1–35.MathSciNetCrossRefzbMATHGoogle Scholar
  7. [7]
    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
  8. [8]
    J. Herbrand, Logical Writings, Harvard University Press, 1972.Google Scholar
  9. [9]
    Dale A. Miller, Proofs in Higher Order Logic, Ph.D. Th., Carnegie-Mellon University, August 1983.Google Scholar
  10. [10]
    Dale A. Miller, Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs. 7th Conference on Automated Deduction, Napa, May 1984.Google Scholar
  11. [11]
    Frank Pfenning. Conversions between Analytic and Non-analytic Proofs. Tech. Report, Carnegie-Mellon University, 1984. (to appear)Google Scholar
  12. [12]
    J.A. Robinson, A machine-oriented logic based on the resolution principle, Journal of the Association for Computing Machinery 12 (1965), 23–41.MathSciNetCrossRefzbMATHGoogle Scholar
  13. [13]
    R. M. Smullyan, First-Order Logic, Springer-Verlag, Berlin, 1968.CrossRefzbMATHGoogle Scholar
  14. [14]
    R. Statman, Lower Bounds on Herbrand’s Theorem, Proceedings of the American Mathematical Society 75 (1979), 104–107.MathSciNetzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Frank Pfenning
    • 1
  1. 1.Departnmnt of MathematicsCarnegie-Mellon UniversityPittsburgh

Personalised recommendations