Blanchette, Jasmin Automation of Logic, MPI for Informatics, Max Planck Society;
Waldmann, Uwe Automation of Logic, MPI for Informatics, Max Planck Society;
Schlichtkrull, A., Blanchette, J., Traytel, D., & Waldmann, U. (2020). Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. Journal of Automated Reasoning, 64, 1169-1195. doi:10.1007/s10817-020-09561-0.