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.
展开▼
