WALDMEISTER : Development of a High Performance Completion-Based Theorem Prover

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.