Divvy: An ATP Meta-system
based on Axiom Relevance Ordering
Motivation, History, and Overview
Two Syntactic Relevance Orderings
Relevance by Symbol Overlap
Relevance by Latent Semantic Analysis
The Divvy ATP Meta-system
Evaluation
Conclusion
The End - Any Questions?
