Lazy and Eager Patterns in High-Performance Automated Theorem Proving

EasyChair Preprint 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 10510},
  year      = {EasyChair, 2023}}