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 [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].