Item

Abstract

We present recent developments within the theorem prover \textsc{Waldmeister}. They 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 ``\textsc{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.