Large-theory premise selection
2 methods in the atlas attack this one problem. They are rivals: each wins something the others do not.
Phrasings that mean this problem
Large-theory premise selection
automated-reasoning
- SInE selectionSymbol-frequency axiom triagespecialistautomated-reasoning
- MePo relevance filterSymbol-overlap scoringspecialistautomated-reasoning