Search

Some general reflections on proof transformations lead to the abstract concept of a quintessential proof of a theorem. A quintessential proof embodies the essential features of many intertranslatable proofs of the theorem. While reasonable candidates for quintessential proofs for normal proofs have been developed, more work is needed with regard to non-normal proofs. Work on proof transformations seems likely to lead to important progress in understanding proofs.

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 a demonstration of TPS, a theorem proving system for classical type theory (Church's typed λ-calculus). TPS can be used 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.

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

In [8] J. A. Robinson introduced a complete refutation pro­cedure called resolution for first order predicate calculus. Resolution is based on ideas in Herbrand’s Theorem, and provides a very convenient framework in which to search for a proof of a wff believed to be a theorem. Moreover, it has proved possible to formulate many refinements of resolution which are still complete but are more efficient, at least in many contexts. However, when efficiency is a prime consideration, the restriction to first order logic is unfortunate, since many state­ments of mathematics (and other disciplines) can be expressed more simply and naturally in higher order logic than in first order logic. Also, the fact that in higher order logic (as in many-sorted first order logic) there is an explicit syntactic distinc­tion between expressions which denote different types of intuitive objects is of great value where matching is involved, since one is automatically prevented from trying to make certain inappropriate matches. (One may contrast this with the situation in which mathematical statements are expressed in the symbolism of axiomatic set theory.)

In [3], [4], and [5] Joyce Friedman formulated and investigated certain rules which constitute a semi-decision procedure for wffs of first order predicate calculus in closed prenex normal form with prefixes of the form ∀x1 ...∀xk∃y1 ...∃Ym∀z1 ...∀z n . Given such a wff QM,where Q is the prefix and M is the matrix in conjunctive normal form, Friedman’s rules can be used, in effect, to construct a matrix M* which is obtained from M by deleting certain conjuncts of M. Obviously, ⊢QM⊃QM* Using the Herbrand-Godel theorem for first order predicate calculus, Friedman showed that ⊢QM if and only if ⊢QM*. Clearly if M* is the empty conjunct (i.e., a tautology), ⊢QM* so ⊢QM. Friedman also showed that for certain classes of wffs, such as those in which m ≤ 2 or n = 0 in the prefix above, ⊢QM if and only if M* is the empty conjunct. Hence for such classes of wffs the rules constitute a decision procedure. Computer implementation [4] of the procedure has shown it to be quite efficient by present standards.