Iterative Lemma Usage

Intuition

• Inspired by Quaife's development with Otter
• Follow your nose through a sequence of lemmas to the conjecture
• Keep only the most powerful lemmas

Three Variants

• Iterative Lemma Addition
  • As lemmas are proved, add to the axioms
  • Can swamp system with redundant lemmas
• Iterative Lemma Replacement
  • As each lemma is proved, replace the previous one
  • Can discard useful lemmas
  • Cannot produce a branching proof structure
• Iterative Lemma Selection
  • Discard previous lemmas that are easily proved
  • Reminiscent of Draeger & Schulz' technique

Strengths and Weaknesses

• Each lemma must be provable from axioms and preceding lemmas
• Likely to fail if proof structure is branching