Dale A. Miller, "A Compact Representation of Proofs," Studia Logica, 46 (1987), 346-370.

Expansion tree proofs for theorems of type theory (without extensionality, choice, and infinity) are introduced. An expansion tree proof is an expansion tree where the deep formula is tautologous and the dependency relation on expansion terms is acyclic. If a formula has an ET-proof, then it has an H-proof (Herbrand proof)--an H-proof is a deduction using tautologies as axioms, and anti-prenexing, existential and universal generalization, lambda expansion, and existential contraction as inference rules. This provides soundness of ET-proofs.

The author also shows how two [dual] expansion trees with the same shallow formula can be merged to give one whose deep formula is implied by the disjunction of the previous deep formulas [implies the conjunction of the previous deep formulas]. This is used to show how ET-proofs for [A or B] and [C or B] can be combined to give an ET-proof for [[A and C] or B]. Similarly, we can obtain an ET-proof for [A or B] from an ET-proof for [A or B or B]. Both of these results are used in the next section on sequential proofs.

A cut-free sequential proof calculus (in the spirit of Gentzen) is presented. The author also considers q-sequents of expansion trees (not just formulas) with dual expansion trees in the antecedent and expansion trees in the succedent, and where the combined expansion trees (with a disjunctive root node and negation nodes preceding the dual trees) is an ET-proof. The author shows how to convert an ET-proof into a sequential proof of the formula. Conversely, the author shows how to convert a sequential proof of a sequent to a q-sequent with the original sequent as shallow formulas (as a special case: formulas with sequential proofs have ET-proofs). This gives soundness and completeness of ET-proofs, as well as a direct method for translating between ET-proofs and more natural sequential proofs.

An ET-proof [P implies Q] of a formula [C implies D] gives a "linear" derivation (in the sense of Craig) which is "balanced"--that is, first we do universal instantiatiations and duplications and lambda contractions, then we do one propositional step ("matrix change"), and end with existential generalizations and simplifications and lambda expansions. As a result, we have a "propositional interpolant" X so that we can prove [C implies X] and [X implies D] and we have every parameter in X occurred either in D and some expansion term in P or in C and some expansion term in Q.

Finally, the author presents the appropriate way to handle Skolem terms (Skolem functions must have necessary arguments and these necessary arguments must not contain variables which become bound) and a notion of a Skolem expansion tree proof (ST-proof). The set of all formulas satisfying these restrictions forms the Herbrand universe. This set is closed under beta reduction. Skolem expansion trees remain Skolem expansion trees under substitution (which was not true of expansion trees). Also, we can dispense with the requirement that the dependency relation be acyclic because the equivalent embedding relation (on selected variables) is explicitly represented by subformulas (of Skolem terms). The author proves soundness and completeness of ST-proofs by showing how to translate back and forth from ET-proofs.