Using Lemmas
Background
- Many problems beyond the reach of (resource limited) ATP
- Prove and use intermediate lemmas
- Lemmas from humans or computers
Iterative Lemma Usage
- ILA:
As lemmas are proved, add to the axioms
- ILR:
As lemmas are proved, replace the previous one
- ILS:
Remove previous lemmas that are easily proved
- Each lemma must be provable from axioms and preceding lemmas
Recursive Lemma Usage
- Set the conjecture as the initial target
- Use axioms and mimimal combinations of lemmas to prove the target
- Selection:
Greedily apply recursively to prove lemmas (and use relevance)
- Minimization:
Tolerant branch-and-bound, with iterative deepening
Evaluation