1 Introduction  
2 Early History  
3 Characterization of Mathematical Knowledge  
4 Premise Selection  
5 Guidance of Saturation-based ATPs  
6 Guidance of Tableaux and Instantiation-based ATPs  
7 Tactic Based ITP Guidance  
8 Related Symbolic Classification Problems  
9 Conclusion