Conclusion

Strengths and Weaknesses

• Working lemma management techniques
• Robust to poorly constituted lemma sets
• Recursive approaches weak with large lemma sets
  • Need to prune large lemma sets
  • Prophet, Draeger & Schulz

Future

• Use AGInT to generate lemmas
• Integrate and test lemma pruning