Relevance, YuCS, and YuLM

Relevance

• Measure relevance of formulae to conjecture
• Based on "aboutness", in terms of symbols

YuCS

• Use relevance to select axioms to form axiom reduced problems
• Uses combinations of groups of axioms

YuLM

• Use relevance to select lemmas to add to problems
• Uses man and machine generated lemmas