High Performance ATP Systems by Combining Several AI Methods

Jörg Denzinger and Marc Fuchs and Matthias Fuchs

appeared in:
Proc. International Joint Conference on Artificial Intelligence (IJCAI) 1997, Nagoya, Morgan Kaufmann, 1997, pp. 102-107.


Abstract

We present a design for an automated theorem prover that controls its search based on ideas from several areas of artificial intelligence (AI). The combination of case-based reasoning, several similarity concepts, a cooperation concept of distributed AI and reactive planning enables a system to learn from previous successful proof attempts. In a kind of bootstrapping process easy problems are used to solve more and more complicated ones. We provide case studies from two domains in pure equational theorem proving. These case studies show that an instantiation of our architecture achieves a high grade of automation and outperforms state-of-the-art conventional theorem provers.



Download extended version of paper (97 Kbytes)

Generated: 29/10/99