Your search returned the following 9 documents:

9. Theory Instantiation
   Harald Ganzinger and Konstantin Korovin
   In: 13th Conference on Logic for Programming Artificial Intelligence Reasoning (LPAR'06), Phnom Penh, Cambodia, 2006, 497-511
   
8. Theory Instantiation
   Harald Ganzinger and Konstantin Korovin
   In: Logic for Programming, Artificial Intelligence, and Reasoning : 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, 2006, 497-511
   
7. Knuth-Bendix constraint solving is NP-complete
   Konstantin Korovin and Andrei Voronkov
   ACM Transactions on Computational Logic 6 (2): 361-388, 2005
   
6. Integration of equational reasoning into instantiation-based theorem proving
   Harald Ganzinger and Konstantin Korovin
   In: Computer science logic : 18th International Workshop CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, 2004, 71-84
   
5. New Directions in Instantiation-Based Theorem Proving
   Harald Ganzinger and Konstantin Korovin
   In: 18th Annual IEEE Symposium on Logic in Computer Science (LICS-03), Ottawa, Canada, old, 2003, 55-64
   [PDF: Download: _03LICS.pdf]
   
4. 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
   
   
3. Orienting rewrite rules with the Knuth-Bendix order
   Konstantin Korovin and Andrei Voronkov
   Information and Computation 183 (2): 165-186, 2003
   
2. 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
   
   
1. Knuth-Bendix orders in automated deduction and term rewriting
   Konstantin Korovin
   Doctoral dissertation, University of Manchester, 2003