WALDMEISTER : Development of a High Performance Completion-Based Theorem Prover
Arnim Buch, Thomas Hillenbrand · 1996
: 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 po...