Lazy and Eager Patterns in High-Performance Automated Theorem Proving

                Stephan Schulz

Eager maintenance of invariants is often the first approach to
implement high-performance data structures. We present a number of
examples from the evolving implementation of the theorem prover E to
demonstrate that a more relaxed, lazy implementation can have
advantages for simplicity, performance, or both. Existing examples
include shared rewriting, term cell garbage collection, and orphan
removal, additional optimisations are identified for term index
maintenance and clause selection.