Weidenbach, Christoph Automation of Logic, MPI for Informatics, Max Planck Society;
https://www.ijcai.org/Proceedings/93-1/Papers/009.pdf (Verlagsversion)
Weidenbach, C. (1993). Extending the Resolution Method with Sorts. In R. Bajcsy (Ed.), Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI '93) (pp. 60-65). Chambery, France: Morgan Kaufmann.