High Performance ATP Systems by Combining Several AI Methods

Abstract

We present a concept for an automated theorem prover that employs a search control 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 using our concept to learn form 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 of interest in pure equational theorem proving taken from the TPTP library. These case studies show that an instantiation of our architecture achiéves a high grade of automation and outperforms state-of-the-art conventional theorem provers.