@Conference{KorovinVoronkov:KnuthBendix:2000,
  author    = {Korovin, K. and Voronkov, A.},
  title     = {A Decision Procedure for the Existential Theory 
               of Term Algebras with the {Knuth-Bendix} Ordering},
  year      = 2000,
  month     = jun,
  address   = {Santa Barbara, California},
  booktitle = {Proc. 15th Annual IEEE Symp. on Logic in Computer Science (LICS'00)},
  pages     = {291-302}}