Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-41624
Titel: Knowledge-based Cooperation between Theorem Provers by TECHS
VerfasserIn: Fuchs, Dirk
Denzinger, Jörg
Sprache: Englisch
Erscheinungsjahr: 1997
Erscheinungsort: Kaiserslautern
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: We present a methodology for coupling several saturation-based theorem provers (running on different computers). The methodology is well-suited for realizing cooperation between different incarnations of one basic prover. Moreover, also different heterogeneous provers -that differ from each other in the calculus and in the heuristic they employ- can be coupled. Cooperation between the different provers is achieved by periodically interchanging clauses which are selected by so-called referees. We present theoretic results regarding the completeness of the system of cooperating provers as well as describe concrete heuristics for designing referees. Furthermore, we report on two experimental studies performed with homogeneous and heterogeneous provers in the areas superposition and unfailing completion. The results reveal that the occurring synergetic effects lead to a significant improvement of performance.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-416240
hdl:20.500.11880/37788
http://dx.doi.org/10.22028/D291-41624
Schriftenreihe: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Band: 97,11
Datum des Eintrags: 5-Jun-2024
Fakultät: SE - Sonstige Einrichtungen
Fachrichtung: SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz
Professur: SE - Sonstige
Sammlung:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Dateien zu diesem Datensatz:
Datei Beschreibung GrößeFormat 
SEKI-Report-SR-97-11_Fuchs-Denzinger_Knowledge=based-Cooperation-between-Theorem-Provers-by-TECHS .pdf1,56 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.