Batch and Limited Selection

Batch Selection

• Select more than one axiom at each iteration
• Reduces effort-per-axiom
• Less focus because context is not updated

Limited Selection

• Consider only some most syntactically relevant axioms for each method
• Produces faster progress
• Gives more weight to syntactic measure