Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-41452
Titel: | Experiments in the Heuristic Use of Past Proof Experience |
VerfasserIn: | Fuchs, Matthias |
Sprache: | Englisch |
Erscheinungsjahr: | 1995 |
Erscheinungsort: | Kaiserslautern |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
Abstract: | Problems stemming from the study of logic calculi in connection with an inference rule called “condensed detachment” are widely acknowledge as prominent test sets for automated deduction systems and their search guiding heuristics. It is in the light of these problems that we demonstrate the power of heuristics that make use of past proof experience with numerous experiments. We present two such heuristics. The first heuristic attempts to re-enact a proof of a proof problem found in the past in a flexible way in order to find a proof of a similar problem. The second heuristic employs “features” in connection with past proof experience to prune the search space. Both these heuristics not only allow for substantial speed-ups, but also make it possible to prove problems that were out of reach when using so-called basic heuristics. Moreover, a combination of these two heuristics can further increase performance. We compare our results with the results the creators of OTTER obtained with this renowned theorem prover and this way substantiate or achievements. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291--ds-414524 hdl:20.500.11880/37773 http://dx.doi.org/10.22028/D291-41452 |
Schriftenreihe: | SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447] |
Band: | 95,10 |
Datum des Eintrags: | 4-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öße | Format | |
---|---|---|---|---|
SEKI-Report-SR-95-10_Fuchs_Experiments-in-the-Heuristic-Use-of-Past-Proof-Experience .pdf | 4,03 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.