Date: Tue, 07 Jan 1997 15:42:07 GMT Server: NCSA/1.4.2 Content-type: text/html Using Knowledge Automatically

Using Knowledge Automatically

The Bledsoe Philosophy of automated theorem proving is basically the belief that automated provers must use human-like methods in order to be successful in mathematics.

When a mathematician tries to prove a theorem, he has the knowledge of thousands of theorems and definitions. He also knows how and when to use them. This is a very difficult process to automate.

Automatic and semi-automatic theorem proving programs which are able to use the knowledge of other theorems and definitions are thereby able to reach arbitrarily far into formalizable mathematics and prove certain types of theorems.

The IPR program provides a method for storing and accessing mathematical knowledge so that an automated theorem proving program can use it effectively. We hope this is a step in the right direction.

The report atp-127.ps by Benjamin Shults reports on some work in this field. See the report atp-127a.ps for more clear description of the framework without the examples.

Since the publication of those papers, other challenges have appeared. If you are particularly interested in this work, then ask me about work in progress.


Do you have feedback or want more information? Contact Benjamin Shults.