Burel, Guillaume Automation of Logic, MPI for Informatics, Max Planck Society;
Burel, G. (2011). Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo. Logical Methods in Computer Science, 7(1): 3, pp. 3:1-3:31. doi:10.2168/LMCS-7 (1:3) 2011.