Korovin, Konstantin Programming Logics, MPI for Informatics, Max Planck Society;
Voronkov, Andrei Programming Logics, MPI for Informatics, Max Planck Society;
Korovin, K., & Voronkov, A. (2005). Knuth-Bendix constraint solving is NP-complete. ACM Transactions on Computational Logic, 6, 361-388.