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