High Performance ATP Systems by Combining Several AI Methods

  • We present a concept for an automated theorem prover that employs a searchcontrol based on ideas from several areas of artificial intelligence (AI). The combi-nation of case-based reasoning, several similarity concepts, a cooperation conceptof distributed AI and reactive planning enables a system using our concept tolearn form previous successful proof attempts. In a kind of bootstrapping processeasy problems are used to solve more and more complicated ones.We provide case studies from two domains of interest in pure equationaltheorem proving taken from the TPTP library. These case studies show thatan instantiation of our architecture achieves a high grade of automation andoutperforms state-of-the-art conventional theorem provers.

Metadaten exportieren

  • Export nach Bibtex
  • Export nach RIS

Weitere Dienste

Teilen auf Twitter Suche bei Google Scholar
Metadaten
Verfasserangaben:Jörg Denzinger, Marc Fuchs
URN (Permalink):urn:nbn:de:hbz:386-kluedo-3669
Schriftenreihe (Bandnummer):SEKI Report (96,9)
Dokumentart:Preprint
Sprache der Veröffentlichung:Englisch
Jahr der Fertigstellung:1996
Jahr der Veröffentlichung:1996
Veröffentlichende Institution:Technische Universität Kaiserslautern
Datum der Publikation (Server):03.04.2000
Fachbereiche / Organisatorische Einheiten:Fachbereich Informatik
DDC-Sachgruppen:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Lizenz (Deutsch):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011

$Rev: 13581 $