Our Lemma Management Techniques
Iterative Lemma Usage
- Relies on lemmas being ordered
- Each lemma must be provable from the axioms and preceding lemmas
- Even if lemmas are not part of final proof structure
- Likely to fail if proof structure is branching
Recursive Lemma Selection and Minimization
- Robust to order of lemmas
- Can cope with unprovable lemmas
- Can cope with unnecessary/irrelevant lemmas
- Independent of proof structure
- Currently ... weak with large lemma sets