Blanchette, Jasmin Christian Automation of Logic, MPI for Informatics, Max Planck Society;
Blanchette, J. C., Haslbeck, M., Matichuk, D., & Nipkow, T. (2015). Mining the Archive of Formal Proofs. In M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, & V. Sorge (Eds.), Intelligent Computer Mathematics (pp. 3-17). Berlin: Springer. doi:10.1007/978-3-319-20615-8_1.