- Claude Kirchner and Pierre Lescanne. Solving disequations. In Proceedings, Symposium on Logic in Computer Science, pages 347-352, Ithaca, New York, 22-25 June 1987. The Computer Society of the IEEE.
- Gerald E. Peterson and Mark E. Stickel. Complete sets of reductions for some equational theories. Journal of the ACM, 28(2):233-264, April 1981.
- J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23-41, January 1965.
- Mark E. Stickel. A unification algorithm for associative-commutative functions. Journal of the ACM, 28(3):423-434, July 1981.