Conclusion

Observations

• Encouraging (but not startling) results
• Will benefit from further refinement and evaluation
• Applications
  • CSSCPA lemma selection in restart
  • As a quality measure in Faust and other ATP systems

Future

• Directed relevance
• Piecewise combining of predicate and functor relevance
• More differentiating statistical evaluation of relevance measures
• Further development and evaluation of YuLM