Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs
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  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 .
Key WordsHigher-order Logic Expansion Trees ET-proofs Natural Deduction Matings
Unable to display preview. Download preview PDF.
- 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
- 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
- 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
-  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
- W. W. Bledsoe, “Using Examples to Generate Instautiations for Set Variables,” University of Texas at Austin Technical Report ATP-67, July 1982.Google Scholar
- Gdrard P. Huet, “A Mechanization of Type Theory,” Proceedings of the Third International Joint Conference on Artificial Intelligence 1973, 139–146.Google Scholar
- 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
- 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
- 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
- Frank Pfenning, “Analytic and Non-analytic Proofs,” elsewhere in these proceedings.Google Scholar