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].
This work was supported by NSF grant MCS81-02870.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Bibliography
Peter B. Andrews, “Resolution in Type Theory,” Journal of Symbolic Logic 36 (1971), 414–432.
Peter B. Andrews, “Provability in Elementary Type Theory,” Zeitschrift für Mathematische Logik und Grundlagen der Mathematlk 20 (1974), 411–418.
Peter B. Andrews and Eve Longlni Cohen, “Theorem Proving in Type Theory,” Proceedings of the Fifth International Joint Conference on Artificial Intelligence 1977, 566.
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.
[5] Peter B. Andrews, “Theorem Proving Via General Matings,” Journal of the Association for Computing Machinery 28 (1981), 193–214.
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.
Wolfgang Bibel, “Matrices with Connections,” Journal of the Association of Computing Machinery 28 (1981), 633–645.
[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.
W. W. Bledsoe, “Using Examples to Generate Instautiations for Set Variables,” University of Texas at Austin Technical Report ATP-67, July 1982.
Alonzo Church, “A Formulation of the Simple Theory of Types,” Journal of Symbolic Logic 5 (1940), 56–68.
Gdrard P. Huet, “A Mechanization of Type Theory,” Proceedings of the Third International Joint Conference on Artificial Intelligence 1973, 139–146.
Gérard P. Huet, “A Unification Algorithm for Typed λ-calculus,” Theoretical Computer Science 1 (1975), 27–57.
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.
D. C. Jensen and T. Pietrzykowski, “Mechanizing ω-Order Type Theory Through Unification,” Theoretical Computer Science 3 (1976), 123–171.
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.
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.
Frank Pfenning, “Analytic and Non-analytic Proofs,” elsewhere in these proceedings.
T. Pietrzykowski and D. C._Jensen, “A complete mechanization of ω-order type theory,” Proceedinqs of the ACM Annual Conference, Volume I, 1972, 82–92.
Tomasz Pietrzykowski, “A Complete Mechanization of Second-Order Type Theory,” Journal of the Association for Computing Machinery 20 (1973), 333–364.
J. A. Robinson, “Mechanizing Higher-Order Logic,” Machine Intelliqence 4, Edinburgh University Press, 1969, 151–170.
Patrick Suppes, Introduction to Logic, D. Van Nostrand Company Ltd., Princeton, 1957.
Moto-o-Takahashi, “A proof of cut-elimination theorem in simple type-theory,” Journal of the Mathematical Society of Japan 19 (1967), 399–410.
Alfred Tarski, “A Lattice-theoretical Fixpoint Theorem and Its Applications,” Pacific Journal of Mathematics 5 (1955), 285–309.
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
Miller, D.A. (1984). Expansion Tree Proofs and Their Conversion to Natural Deduction 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_22
Download citation
DOI: https://doi.org/10.1007/978-0-387-34768-4_22
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