We describe and prove completion procedures for equational term rewriting systems in order-sorted algebras, using the technique of proof orderings. Problems specific to order-sorted equational logic are emphasized. © 1990.
Gnaedig, I., Kirchner, C., & Kirchner, H. (1990). Equational completion in order-sorted algebras. Theoretical Computer Science, 72(2–3), 169–202. https://doi.org/10.1016/0304-3975(90)90034-F