- prove some theorems
- learn axiom selection from successful proofs
- select less/better axioms for new proof attempts
- prove some more theorems
- loop
- many AI possibilities for selection of axioms, lemma discovery, etc.
- funny behavior on Isabelle/Sledgehammer data on first try, then also large improvements
Josef Urban
2011-01-14