Search

This is a slightly enhanced version of the acceptance speech given by the author after receiving the Herbrand Award at the 19th International Conference on Automated Deduction (CADE-19) in Miami, Florida, on August 1, 2003. Historical matters related to Herbrand's theorem, higher-order logic, and the author's work are discussed. Contributions by others that have been helpful to the author are noted.

This is description of TPS, a theorem-proving system for classical type theory (Church's typed λ-calculus). TPS has been designed to be a general research tool for manipulating wffs of first- and higher-order logic, and searching for proofs of such wffs interactively or automatically, or in a combination of these modes. An important feature of TPS is the ability to translate between expansion proofs and natural deduction proofs. Examples of theorems that TPS can prove completely automatically are given to illustrate certain aspects of TPS's behavior and problems of theorem proving in higher-order logic.

TPS is an automated theorem proving system which can be used to prove theorems of first- or higher-order logic automatically, interactively, or in a combination of these modes of operation. Proofs in TPS are presented in natural deduction style. ETPS is a program which was obtained from TPS by deleting all the facilities for proving theorems automatically. ETPS can be used by students to learn how to prove theorems interactively. The objective of the tutorial is to teach participants how to make effective use of TPS and ETPS.

This is a brief update on the Tps automated theorem proving system for classical type theory, which was described in [3]. Manuals and information about obtaining Tps can be found at http://gtps.math.cmu.edu/tps.html.

When searching for proofs of theorems which contain definitions, it is a significant problem to decide which instances of the definitions to instantiate. We describe a method called dual instantiation, which is a partial solution to the problem in the context of the connection method; the same solution may also be adaptable to other search procedures. Dual instantiation has been implemented in TPS, a theorem prover for classical type theory, and we provide some examples of theorems that have been proven using this method. Dual instantiation has the desirable properties that the search for a proof cannot possibly fail due to insufficient instantiation of definitions, and that the natural deduction proof which results from a successful search will contain no unnecessary instantiations of definitions. Furthermore, the time taken by a proof search using dual instantiation is in general comparable to the time taken by a search in which exactly the required instances of each definition have been instantiated. We also describe how this technique can be applied to the problem of instantiating set variables.

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.

A procedure is given for transforming refutation matings into natural deduction proofs. Thus a theorem proving system which establishes the validity of a theorem by the general matings approach can apply this procedure to obtain a comprehensible proof of the theorem without further search. This illuminates the close relationship between matings and proofs, and serves as a step toward a synthesis between apparently quite different approaches to automated theorem proving.

Theorem proving is difficult and deals with complex phenomena. The difficulties seem to be compounded when one works with higher-order logic, but the rich expressive power of Church's formulation [10] [3] of this language makes research on theorem proving in this realm very worthwhile. In order to make significant progress on this problem, we need to try many approaches and ideas, and explore many questions. A highly relevant question is "What makes a logical formula valid?".

When one is seeking an expansion proof for a theorem of higher-order logic, not all necessary substitution terms can be generated by unification of formulas already present, so certain expansion options [5] are applied, and then a search for a p-acceptable mating [2] is made, using Huet's higher-order unification algorithm [8] to generate all remaining substitution terms. The expansion options consist of quantifier duplications and projective and primitive substitutions (such as

It is shown by a purely syntactic argument how the completeness of resolution in type theory implies the consistency of type theory with axioms of extensionality, descriptions, and infinity. In this system the natural numbers are defined, and Peanos Postulates proved; indeed, classical analysis and much more can be formalized here. Nevertheless, Godels results show that the completeness of resolution in type theory cannot be proved in this system. Mathematical Offprint Service classification numbers: O2B15 Higher order predicate calculus O2G99 Methodology of deductive systems 68A40 Theorem proving This research was partially supported by NSF Grant GJ-28457X. Resolution and the Consistency of Analysis Peter B. Andrews §