Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-41610
Titel: Coupling Saturation-Based Provers by Exchanging Positive/Negative Information
VerfasserIn: Fuchs, Dirk
Sprache: Englisch
Erscheinungsjahr: 1997
Erscheinungsort: Kaiserslautern
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: We examine different possibilities of coupling saturation-based theorem provers by exchanging positive/negative information. We discuss which positive or negative information is well-suited for cooperative theorem proving and show in an abstract way how this information can be used. Based on this study, we introduce a basic model for cooperative theorem proving. We present theoretical results regarding the exchange of positive/negative information as well as practical methods and heuristics that allow for a gain of efficiency in comparison with sequential provers. Finally, we report on experimental studies conducted in the areas condensed detachment, unfailing completion, and superposition.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-416107
hdl:20.500.11880/37823
http://dx.doi.org/10.22028/D291-41610
Schriftenreihe: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Band: 97,7
Datum des Eintrags: 6-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



Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.