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



Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.