Date: Tue, 07 Jan 1997 15:42:11 GMT Server: NCSA/1.4.2 Content-type: text/html Benji's ATP research page

ATP research

The IPR System

The IPR system proves theorems in mathematics by using a knowledge base of theorems, axioms and definitions. Rather than applying all of its knowledge systematically, the IPR prover picks a single bit of information at a time according to its determination of the current usefulness of the information.

The IPR Framework

IPR uses the tableaux-calculus for first-order logic theorem proving. This method has some properties which recommend its use by provers which are intended to communicate with non-expert humans. A branch of a tableau can be displayed as a sequent.

The knowledge is stored in the knowledge base in the form of sequents. When the theorem prover reaches the q-limit, it chooses a branch of the tableau which needs more work and searches the knowledge base for the most useful bit of information. It determines which theorem to use by comparing the branch (as a sequent) to the theorems in the knowledge base.

The success of the prover on traditionally difficult problems shows that this method of storing and fetching theorems has merit.

Two tech reports offer more information about the IPR framework. [Intelligent use of a knowledge base in automated theorem proving.,Challenge problems in first-order theories.] I am currently preparing more papers for submission. I will attach some of these reports to this page as soon as possible.

The English Interface

All of the output from IPR is in English. When it finds a proof, it outputs a description of the steps it took and the theorems it applied in a form which might appear in a textbook. If the user chooses to interact during the theorem-proving process, IPR displays each branch of the proof in English. For example:

Suppose all of the following:
1. (_B) is a linearly independent subset of the vector space (_V)
2. (_B0) is a basis of the vector space (_V)
and show that
the union of E and F is a basis of the vector space (_V)
Here, (_B), (_B0) and (_V) represent constants and E and F are variables.

Examples of Proofs

The first hard theorem IPR proved in 1994 was the 101st labeled theorem from John Kelley's General Topology:

If a product is locally compact, then each coordinate space is locally compact.

IPR proved this in the presence of 100 theorems. Each of the theorems were taken from earlier sections of the text related to the predicates involved in the theorem. IPR analyses the knowledge base once for each formula in the proof. When it needs to apply a theorem, it compares the usefulness of the theorems to the current situation and choses the single theorem which if considers most useful. In this proof, IPR did not use any of the theorems except the three which are needed in the proof. It chose those theorems and found the shortest possible proof without wasting any time on the other knowledge.

A second example, this one involving much more complex reasoning, is the following:

If S is a Hausdorff topological space, then the diagonal of SXS is closed.

The proof of this theorem (given a certain knowledge base) requires the application of twelve theorems. The proof also requires some equality reasoning and a fairly tricky variable instantiation. This variable instantiation is needed because the proof involves finding an open set in SXS containing an arbitrary point in SXS and disjoint from the diagonal.

In the presence of a knowledge base containing over 12 theorems, IPR finds this proof in under a minute on my PC at home.

Since my dissertation will be on this topic, expect this part of the web to grow.

This work was done as part of the Automated Theorem Proving Group at The University of Texas at Austin.


Benjamin Shults