Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-41574
Titel: | WALDMEISTER : Development of a High Performance Completion-Based Theorem Prover |
VerfasserIn: | Buch, Arnim Hillenbrand, Thomas |
Sprache: | Englisch |
Erscheinungsjahr: | 1996 |
Erscheinungsort: | Kaiserslautern |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
Abstract: | In this report we give an overview of the development of our new WALDMEISTER prover for equational theories. We elaborate a systematic stepwise design process, starting with the inference system for unfailing Knuth-Bendix completion and ending up with an implementation which avoids the main diseases today's provers suffer from: overindulgence in time and space. Our design process is based on a logical three-level system model consisting of basic operations for inference step execution, aggregated inference machine, and overall control strategy. Careful analysis of the inference system for unfailing completion has revealed the crucial points responsible for time and space consumption. For the low level of our model, we introduce specialized data structures and algorithms speeding up the running system and cutting it down in size - both by one order of magnitude compared with standard techniques. Flexible control of the mid-level aggregation inside the resulting prover is made possible by a corresponding set of parameters. Experimental analysis shows that this flexibility is a point of high importance. We go on with some implementation guidelines we have found valuable in the field of deduction. The resulting new prover shows that our design approach is promising. We compare our system's throughput with that of an established system and finally demonstrate how two very hard problems could be solved by WALDMEISTER. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291--ds-415748 hdl:20.500.11880/37835 http://dx.doi.org/10.22028/D291-41574 |
Schriftenreihe: | SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447] |
Band: | 96,1 |
Datum des Eintrags: | 10-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-96-01_Buch-Hillenbrand_Waldmeister-Development-of-a-High-Performance-Completion=Based-Theorem-Prover.pdf | 4,01 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.