- Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201-215, July 1960.
- Vincent J. Digricoli and Malcolm C. Harrison. Equality-based binary resolution. Journal of the ACM, 33(2):253-289, April 1986.
- Gérard Huet. Confluent reductions: Abstract properties and application to term rewriting systems. Journal of the ACM, 27(4):797-821, October 1980.
- Greg Nelson and Derek C. Oppen. Fast decision procedures based on congruence closure. Journal of the ACM, 27(2):356-364, April 1980.
- 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.
- James R. Slagle. Automatic theorem proving with built-in theories including equality, partial ordering, and sets. Journal of the ACM, 19(1):120-135, January 1972.
- Mark E. Stickel. A unification algorithm for associative-commutative functions. Journal of the ACM, 28(3):423-434, July 1981.
- Lawrence Wos, George A. Robinson, Daniel F. Carson, and Leon Shalla. The concept of demodulation in theorem proving. Journal of the ACM, 14(4):698-709, October 1967.