On Connections and Higher-Order Logic

This is an expository introduction to an approach to theorem proving in higher-order logic based on establishing appropriate connections between subformulas of an expanded form of the theorem to be proved. Expansion trees and expansion proofs play key roles