Your search returned the following 10 documents:

10. Knuth-Bendix constraint solving is NP-complete
    Konstantin Korovin and Andrei Voronkov
    ACM Transactions on Computational Logic 6 (2): 361-388, 2005
    
9. Orienting Equalities with the Knuth-Bendix Order
   Konstantin Korovin and Andrei Voronkov
   In: 18th Annual IEEE Symposium on Logic in Computer Science (LICS-03), Ottawa, Canada, June, 22 - June, 25, 2003, 75-84
   
   
8. Orienting rewrite rules with the Knuth-Bendix order
   Konstantin Korovin and Andrei Voronkov
   Information and Computation 183 (2): 165-186, 2003
   
7. AC-compatible Knuth-Bendix Order
   Konstantin Korovin and Andrei Voronkov
   In: Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, Miami, Florida, July, 30 - August, 2, 2003, 47-59
   
   
6. On the Evaluation of Indexing Techniques for Theorem Proving
   Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, and Andrei Voronkov
   In: Automated reasoning : First International Joint Conference, IJCAR 2001, Siena, Italy, June, 18-22, 2001, 257-271
   [PS: Download: evaluation.ps]
   
5. Decidability and Complexity of Simultaneous Rigid E-unification with One Variable and Related Results
   Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, and Andrei Voronkov
   Theoretical Computer Science 243 (1/2): 167-184, 2000
   
4. The ground-negative fragment of first-order logics is $\pi^p_2$-complete
   Andrei Voronkov
   The Journal of Symbolic Logic 64 (3): 984-990, 1999
   
3. Complexity of Nonrecursive Logic Programs with Complex Values
   Sergei Vorobyov and Andrei Voronkov
   In: Proceedings of the 17th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS-98), Saeattle, Washington, U.S.A., June 1-4, 1998, 1998, 244-253
   
   
2. Elimination of Equality via Transformation with Ordering Constraints
   Leo Bachmair, Harald Ganzinger, and Andrei Voronkov
   In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), Lindau, Germany, July, 5-10 1998, 1998, 175-190. Note: Short version of MPI-I-97-2-012
   
1. The Decidability of Simultaneous Rigid E-Unification with One Variable
   Anatoli Degtyarev, Yuri Gurevich, Paliath Narendran, Margus Veanes, and Andrei Voronkov
   In: Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA-98), Tsukuba, Japan, March 30 - April 1, 1998, 1998, 181-195