Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs

  • Dale A. Miller
Part of the Lecture Notes in Computer Science book series (LNCS, volume 170)


We present a new form of Herbrand’s theorem which is centered around structures called expansion trees. Such trees contains substitution formulas and selected (critical) variables at various non-term/hal nodes. These trees encode a shallow formula and a deep formula — the latter containing the formulas which label the terminal nodes of the expansion tree. If a certain relation among the selected variables of an expansion tree is acycllc and if the deep formula of the tree is tantologous, then we say that the expansion tree is a special kind of proof, called an ET-proof, of its shallow formula. Because ET-proofs are suf~ciently simple and general (expansion trees are, in a sense, generalized formulas), they can be used in the context of not only first-order logic but also a version of higher-order logic which properly contains first-order logic. Since the computational logic literature has seldomly dealt with the nature of proofs in higher-order logic, our investigation of ET-proofs will be done entirely in this setting. It can be shown that a formula has an ET-proof if and only if that formula is a theorem of higher-order logic. Expanslon trees have several pleasing practical and theoretical properties. To demonstrate this fact, we use ET-proofs to extend and complete Andrews’ procedure [4] for automatically constructing natural deductions proofs. We shall also show how to use a mating for an ET-proof’s tautologous, deep formula to provide this procedure with the “look ahead” needed to determine if certain lines are unnecessary to prove other lines and when and how backchalning can be done. The resulting natural deduction proofs are generally much shorter and more readable than proofs build without using this mating information. This conversion process works without needing any search. Details omitted in this paper can be found in the author’s dissertation [16].

Key Words

Higher-order Logic Expansion Trees ET-proofs Natural Deduction Matings 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Peter B. Andrews, “Resolution in Type Theory,” Journal of Symbolic Logic 36 (1971), 414–432.MathSciNetCrossRefzbMATHGoogle Scholar
  2. [2]
    Peter B. Andrews, “Provability in Elementary Type Theory,” Zeitschrift für Mathematische Logik und Grundlagen der Mathematlk 20 (1974), 411–418.MathSciNetCrossRefzbMATHGoogle Scholar
  3. [3]
    Peter B. Andrews and Eve Longlni Cohen, “Theorem Proving in Type Theory,” Proceedings of the Fifth International Joint Conference on Artificial Intelligence 1977, 566.Google Scholar
  4. [4]
    Peter B. Andrews, “Transforming Matings into Natural Deduction Proofs,” Fifth Conference on Automated Deduction, Les Arcs, France, edited by W. Bibel and R. Kowalski, Lecture Notes in Computer Science, No. 87, Springer-Verlag, 1980, 281–292.Google Scholar
  5. [5] Peter B. Andrews, “Theorem Proving Via General Matings,” Journal of the Association for Computing Machinery 28 (1981), 193–214.MathSciNetCrossRefzbMATHGoogle Scholar
  6. [6]
    Maria Virginia Aponte, José AlbertoFernández, and Philippe Roussel, “Editing First-order Proofs: Programmed Rules vs. Derived Rules,” Proceedinfs of the 1984 International Symposium on Logic Programming, 92–97.Google Scholar
  7. [7]
    Wolfgang Bibel, “Matrices with Connections,” Journal of the Association of Computing Machinery 28 (1981), 633–645.MathSciNetCrossRefzbMATHGoogle Scholar
  8. [8] W. W. Bledsoe, “A Maximal Method for Set Variables in Automatic Theorem-proving,” in Machine Intelligence g, edited by J. E. Hayes, Donald Michie, and L. I. Mikulich, EllisHorwood Ltd., 1979, 53–100.Google Scholar
  9. [9]
    W. W. Bledsoe, “Using Examples to Generate Instautiations for Set Variables,” University of Texas at Austin Technical Report ATP-67, July 1982.Google Scholar
  10. [10]
    Alonzo Church, “A Formulation of the Simple Theory of Types,” Journal of Symbolic Logic 5 (1940), 56–68.MathSciNetCrossRefzbMATHGoogle Scholar
  11. [11]
    Gdrard P. Huet, “A Mechanization of Type Theory,” Proceedings of the Third International Joint Conference on Artificial Intelligence 1973, 139–146.Google Scholar
  12. [12]
    Gérard P. Huet, “A Unification Algorithm for Typed λ-calculus,” Theoretical Computer Science 1 (1975), 27–57.MathSciNetCrossRefzbMATHGoogle Scholar
  13. [13]
    Gerhard Gentsen, “Investigations into Logical Deductions,” in The Collected Psperu of Gerhard Gentzen, edited by M. E. Szabo, North-Holland Publishing Co., Amsterdam, 1969, 68–131.Google Scholar
  14. [14]
    D. C. Jensen and T. Pietrzykowski, “Mechanizing ω-Order Type Theory Through Unification,” Theoretical Computer Science 3 (1976), 123–171.MathSciNetCrossRefzbMATHGoogle Scholar
  15. [15]
    Dale A. Miller, Eve Longini Cohen, and Peter B. Andrews, “A Look at TPS,” 6th Conference on Automated Deduction, New York, edited by Donald W. Loveland, Lecture Notes in Computere and Science, No. 138, Springer-Verlag, 1982, 50–69.Google Scholar
  16. [16]
    Dale A. Miller, “Proofs in Higher-order Logic,” Ph. D. Dissertation, Carnegie-Mellon University, August 1983. Available as Technical Report MS-CIS-83-37 from the Department of Computer and Information Science, University of Pennsylvania.Google Scholar
  17. [17]
    Frank Pfenning, “Analytic and Non-analytic Proofs,” elsewhere in these proceedings.Google Scholar
  18. [18]
    T. Pietrzykowski and D. C._Jensen, “A complete mechanization of ω-order type theory,” Proceedinqs of the ACM Annual Conference, Volume I, 1972, 82–92.CrossRefGoogle Scholar
  19. [19]
    Tomasz Pietrzykowski, “A Complete Mechanization of Second-Order Type Theory,” Journal of the Association for Computing Machinery 20 (1973), 333–364.MathSciNetCrossRefzbMATHGoogle Scholar
  20. [20]
    J. A. Robinson, “Mechanizing Higher-Order Logic,” Machine Intelliqence 4, Edinburgh University Press, 1969, 151–170.MathSciNetzbMATHGoogle Scholar
  21. [21]
    Patrick Suppes, Introduction to Logic, D. Van Nostrand Company Ltd., Princeton, 1957.zbMATHGoogle Scholar
  22. [22]
    Moto-o-Takahashi, “A proof of cut-elimination theorem in simple type-theory,” Journal of the Mathematical Society of Japan 19 (1967), 399–410.MathSciNetCrossRefzbMATHGoogle Scholar
  23. [23]
    Alfred Tarski, “A Lattice-theoretical Fixpoint Theorem and Its Applications,” Pacific Journal of Mathematics 5 (1955), 285–309.MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • Dale A. Miller
    • 1
  1. 1.Department of Computer and Information ScienceUniversity of PennsylvaniaPhiladelphia

Personalised recommendations