Blanchette, Jasmin Christian Automation of Logic, MPI for Informatics, Max Planck Society;
Waldmann, Uwe Automation of Logic, MPI for Informatics, Max Planck Society;
https://www.isa-afp.org/browser_info/current/AFP/Ordered_Resolution_Prover/document.pdf (出版社版)
Schlichtkrull, A., Blanchette, J. C., Traytel, D., & Waldmann, U. (2018). Formalization of Bachmair and Ganzinger's Ordered Resolution Prover. Archive of Formal Proofs.
