Automating Higher-Order Logic
Peter B. Andrews, Dale Armin Miller, Eve Longini Cohen, Frank Pfenning · Contemporary mathematics - American Mathematical Society · 1984
An automated theorem-proving system called TPS for proving theorems of first or higher-order logic in automatic, semi-automatic, or interactive mode has been developed. As its logical language TPS uses Church's formulation of type theory with A-notation, in which most theorems of mathematics can be expressed very directly. As an interactive tool TPS has many features which facilitate writing formal proofs and manipulating and displaying formulas of logic in traditional notations. In automatic mode TPS combines theorem-proving methods for first-order logic with Huet's unification algorithm for typed A-calculus, finds acceptable general matings (which represent the essential syntactic combinatorial information implicit in proofs), and constructs proofs in natural deduction style. Among the theorems which can· be proved completely automatically is - 3G 'dF 3J [[G J] = F], which expresses Cantor's Theorem that a set ou 0' , has more subsets than members by asserting that there is no function G from individuals to sets which has every set F of individuals in its range. The computer substitutes for F the formula [AW - G W W], which denotes 0' L ou the set {W I W ~ G W} and expresses the key idea in the classical diagonal argument. The methods presently used by TPS in automatic mode are in principle complete for first-order logic, but not for higher-order logic. A recently proved extension of Herbrand's Theorem to type theory is presented. It is anticipated that this metatheorem will provide a basis for extending the capabilities of TPS.