---
title: "High Performance ATP Systems by Combining Several AI Methods"
authors:
  - "Jörg Denzinger"
  - "Marc Fuchs"
  - "Matthias Fuchs"
doi: ""
url: "https://ijcai.org/proceedings/1997/16"
pdf: "https://ijcai.org/proceedings/1997/0016.pdf"
venue: "Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence"
year: 1997
pages: "102-106"
track: "Automated Reasoning"
keywords:
---

# High Performance ATP Systems by Combining Several AI Methods

Jörg Denzinger, Marc Fuchs, Matthias Fuchs

*Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence*, pages 102-106.

## 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 equationa l theorem proving. Th ese case studies show that an instantiation of our architecture achieves a high grade of automation and outperforms state-of-the-art conventional theorem provers.