- Leo Bachmair and Nachum Dershowitz. Inference rules for rewrite-based first-order theorem proving. In Proceedings, Symposium on Logic in Computer Science, pages 331-337, Ithaca, New York, 22-25 June 1987. The Computer Society of the IEEE.
- Alexandre Boudet, Jean-Pierre Jouannaud, and Manfred Schmidt-Schauß Unification in free extensions of Boolean rings and Abelian groups. In Proceedings, Third Annual Symposium on Logic in Computer Science, pages 121-130, Edinburgh, Scotland, 5-8 July 1988. IEEE Computer Society.
- Hubert Comon. Solving inequations in term algebras (extended abstract). In Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, pages 62-69, Philadelphia, Pennsylvania, 4-7 June 1990. IEEE Computer Society Press.
- J. Gallier, W. Snyder, P. Narendran, and D. Plaisted. Rigid E-unification is NP-complete. In Proceedings, Third Annual Symposium on Logic in Computer Science, pages 218-227, Edinburgh, Scotland, 5-8 July 1988. IEEE Computer Society.
- Gérard Huet. Confluent reductions: Abstract properties and application to term rewriting systems. Journal of the ACM, 27(4):797-821, October 1980.
- Jean-Pierre Jouannaud and Emmanuel Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1):1-33, July 1989.
- 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.
- David A. Plaisted. Semantic confluence tests and completion methods. Information and Control, 65(2/3):182-215, May/June 1985.