Tags:automated theorem proving, efficient algorithms and implementation of logics
Abstract:
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.
Lazy and Eager Patterns in High-Performance Automated Theorem Proving
Lazy and Eager Patterns in High-Performance Automated Theorem Proving
