High Performance ATP Systems by Combining Several AI Methods
Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence. Automated Reasoning. 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.
@inproceedings{ijcai1997p16,
title = {High Performance ATP Systems by Combining Several AI Methods},
author = {Denzinger, Jörg and Fuchs, Marc and Fuchs, Matthias},
booktitle = {Proceedings of the Fifteenth International Joint Conference on
Artificial Intelligence, {IJCAI-97}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Martha E. Pollack},
pages = {102--106},
year = {1997},
note = {Automated Reasoning},
url = {https://ijcai.org/proceedings/1997/16},
}
TY - CPAPER TI - High Performance ATP Systems by Combining Several AI Methods AU - Denzinger, Jörg AU - Fuchs, Marc AU - Fuchs, Matthias T2 - Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, IJCAI-97 PB - International Joint Conferences on Artificial Intelligence PY - 1997 SP - 102 EP - 106 UR - https://ijcai.org/proceedings/1997/16 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
