@phdthesis{Korovin:PhD:03,
  author = {Korovin, K.},
  title  ={{Knuth--Bendix} orders in automated deduction
           and term rewriting},
  school={University of Manchester},
  year = 2003
}