Date: Tue, 07 Jan 1997 15:42:07 GMT Server: NCSA/1.4.2 Content-type: text/html
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.