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