Download PDFOpen PDF in browser

Lazy and Eager Patterns in High-Performance Automated Theorem Proving

EasyChair Preprint 10510

5 pagesDate: July 8, 2023

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

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@booklet{EasyChair:10510,
  author    = {Stephan Schulz},
  title     = {Lazy and Eager Patterns in High-Performance Automated Theorem Proving},
  howpublished = {EasyChair Preprint 10510},
  year      = {EasyChair, 2023}}
Download PDFOpen PDF in browser