The New WALDMEISTER Loop at Work

摘要

We present recent developments within the equational theorem prover WALDMEISTER, an implementation of unfailing Knuth-Bendix completion [BDP89] with refinements towards ordered completion. The new developments rely on a novel organization of the underlying saturation-based proof procedure into a system architecture. As is known, the saturation process tends to quickly fill the memory available unless preventive measures are employed. To overcome this problem, our new "WALDMEISTER loop" features a highly compact representation of the search state, exploiting its inherent structure. The implementation just being available, the cost and the benefits of the concept now can exactly be measured. Indeed are our expectations met concerning the drastic cut-down of memory usage with only moderate overhead of time. In addition it has turned out that the revealed structure of the search state paves the way to an easily implemented parallelization of the prover with modest communication requirements and rewarding speed-ups. In order to minimize communication-related latencies, we discuss some variations of the loop to maximally profit from multiple processors. All in all, these innovations allow to solve proof tasks that were previously out of reach. For a summary of the basic features of the system see [LH02]. Here we focus on new achievements that mark a milestone in the development of the system.