PRL Seminars 1998-99

Abstract

Proof planning is an alternative to classical theorem proving in Artificial Intelligence. It has been invented to guide automated search intelligently. I discuss problems of proof planning and their solutions including the design of methods, the integration of external reasoners, and the need of explicit control knowledge. I'll briefly explain why proof plans are well-suited for for proof presentation, and as a basis for theorem proving by analogy. I illustrate the approach for the class of limit theorems.

The knowledge-based proof planning is implemented as a service in the net-based Omega system which we can run (evenings when the net is not too busy) from Cornell via http://www.ags.uni-sb.de/~omega.