非表示:
キーワード:
-
要旨:
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.
