Lazy and Eager Patterns in High-Performance Automated Theorem Proving

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.