Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs

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

Abstract

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

Bibliography

1. [1]
Peter B. Andrews, “Resolution in Type Theory,” Journal of Symbolic Logic 36 (1971), 414–432.
2. [2]
Peter B. Andrews, “Provability in Elementary Type Theory,” Zeitschrift für Mathematische Logik und Grundlagen der Mathematlk 20 (1974), 411–418.
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.
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.
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.
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.
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.
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.
19. [19]
Tomasz Pietrzykowski, “A Complete Mechanization of Second-Order Type Theory,” Journal of the Association for Computing Machinery 20 (1973), 333–364.
20. [20]
J. A. Robinson, “Mechanizing Higher-Order Logic,” Machine Intelliqence 4, Edinburgh University Press, 1969, 151–170.
21. [21]
Patrick Suppes, Introduction to Logic, D. Van Nostrand Company Ltd., Princeton, 1957.
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.
23. [23]
Alfred Tarski, “A Lattice-theoretical Fixpoint Theorem and Its Applications,” Pacific Journal of Mathematics 5 (1955), 285–309.