Recursive Lemma Minimization

Intuition

• Maintain robustness of recursive lemma selection
• Optimize proof w.r.t. lemmas used or CPU time taken
• Branch-and-bound over developing alternative proof structures

• Maintain a list of alternative proof candidates
  
  • Each candidate has a target queue of unproved lemmas
  • Initial proof candidate has the conjecture in its target queue
• Pop target formula from current candidate's target queue
• Form helper sets of increasing size, starting at 0
  • If/when the target formula can be proved from axioms and helper set
    • Find all successful helper sets of that size, and stop
• Form new proof candidates by appending helpers to current candidate's target queue
• If quality of the best new candidate is within tolerance factor of the best on the alternatives list
  • Add other new candidates to the alternatives list
  • Iterate with that best new candidate
  Else
  • Add all new candidates to the alternatives list
  • Iterate with best candidate on the alternatives list
• Stop when current candidate has an empty queue

Strengths and Weaknesses

• Finds a proof structure within tolerance factor of optimal
• Maintains robustness of recursive lemma selection
• More stable than recursive lemma selection
• Can be tuned using tolerance factor