Use of Lemmas

Previous Efforts

• Humans
• Model elimination [Astrachan, Fuchs, etc]
• Adding lemmas before [Draeger & Schulz]
• Adding lemmas during [E-SETHEO]
• Breaking down a problem [Veroff]

Our Approach

• Provide a set of lemmas
• Prove theorem from axioms and selected lemmas
• Prove selected lemmas recursively

The Output

• Combine component proofs to form proof from axioms
• View at proof structure level - axioms, lemmas, theorem
  • Proof structure may be linear or branching
• View at detailed level - details of component proofs