Search

ETPS (Educational Theorem Proving System) is a program that logic students can use to write formal proofs in first-order logic or higher-order logic. It enables students to concentrate on the essential logical problems involved in proving theorems, and it automatically checks the proofs.

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.

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.

Results are obtained about special cases of the decision problem for provability in type theory with A-conversion, minus axioms of extensionality, descriptions, choice, and infinity. |&£ . . . ag [A=g] iff there is a substitution 0 such that 9 * A = 0 * B. Hence fA = g iff A conv Jg. This shows the independence of the axioms of extensionality. If £ is quantifier-free, fVjc . . . Vx Q iff r}C is tautologous. Inhere is no decision procedure for the class of wffs of the form 3z [A=B] , or the class of wffs of the form 3g£* where C is quantifier-free. Hence the only solvable classes of wffs in prenex normal form defined solely by the structure of the prefix are those in which no existential quantifiers occur. PROVABILITY IN ELEMENTARY TYPE THEORY by Peter B. Andrews §

A refinement of the resolution method for mechanical theorem proving is presented. A resolvent C of clauses A and B is called a merge if literals from A and B merge together to form some literal of C . It is shown that the resolution method remains complete if it is required that two noninitial clauses which are not merges never be resolved with one another. It is also shown that this strategy can be combined with the set-of-support strategy.

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 §

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.