Lazy and Eager Patterns in High-Performance Automated Theorem Proving

EasyChair Preprint no. 10510

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.

Keyphrases: automated theorem proving, efficient algorithms, implementation of logics

@Booklet{EasyChair:10510,
  author = {Stephan Schulz},
  title = {Lazy and Eager Patterns in High-Performance Automated Theorem Proving},
  howpublished = {EasyChair Preprint no. 10510},

  year = {EasyChair, 2023}}