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.This is an extended version of a lecture presented to the 8th International Conference on Automated Deduction in Oxford, England on 27 July 1986. This material is based upon work supported by the National Science Foundation under grants DCR-8402532 and CCR-8702699.