@Inproceedings{KorovinVoronkov:CADE03:ACKBO,
  author ={Korovin, K. and Voronkov, A.},
  title ={An {AC}-compatible {Knuth--Bendix} Order},
  year =         2003,
  booktitle =   {19th International Conference on Automated Deduction (CADE'03)},
  pages =        {47 -- 59},
  publisher =   Springer,
  volume = 2741
}