High Performance ATP Systems by Combining Several AI Methods Joerg Denzinger, Matthias Fuchs Fachbereich Informatik, Universitaet Kaiserslautern D-67663 Kaiserslautern Germany E-mail: denzinge@informatik.uni-kl.de, fuchs@informatik.uni-kl.de Marc Fuchs Fakultaet fuer Informatik, TU Muenchen D-80290 Muenchen GERMANY E-mail: fuchsm@informatik.tu-muenchen.de 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 achieves a high grade of automation and outperforms state-of- the-art conventional theorem provers. Keywords theorem proving, machine learning, case-based reasoning, distributed AI, planning Source anonymous FTP server ftp.uni-kl.de [131.246.94.94] path: /reports_uni-kl/computer_science/SEKI/1996/ file: Denzinger.SR-96-09.ps.gz