@comment{{This file has been generated by bib2bib 1.96}}

@comment{{Command line: /usr/bin/bib2bib -c '$key="korovin02unif" or $key="korovin01icalp" or $key="korovin02fsttcs" or $key="zhang05cade" or $key="korovin00lics" or 1=2' ../biblio/abbrevs.bib ../biblio/rtaloop.bib ../biblio/crossrefs.bib}}

@string{ieee = {IEEE}}

@string{springer = {Springer-Verlag}}

@string{lncs = {Lecture Notes in Computer Science}}

@string{univiowa = {University of Iowa}}

@string{deptcsiowa = {Department of Computer Science, } # univiowa}

@inproceedings{korovin01icalp,
  title = {{K}nuth-{B}endix Constraint Solving Is {NP}-Complete},
  author = {Konstantin Korovin and Andrei Voronkov},
  crossref = {icalp01},
  pages = {979--992}
}

@inproceedings{korovin00lics,
  title = {A Decision Procedure for the Existential Theory of Term Algebras
            with the {K}nuth-{B}endix Ordering},
  author = {Konstantin Korovin and Andrei Voronkov},
  crossref = {lics00},
  pages = {291--302}
}

@inproceedings{korovin02unif,
  title = {The Decidability of the First-Order Theory of the {K}nuth-{B}endix
              orders in the case of unary signatures},
  author = {Konstantin Korovin and Andrei Voronkov},
  crossref = {unif02},
  pages = {45--46}
}

@inproceedings{korovin02fsttcs,
  title = {The decidability of the first-order theory of the
             {K}nuth-{B}endix orders in the case of unary signatures},
  author = {Konstantin Korovin and Andrei Voronkov},
  crossref = {fsttcs02},
  note = {A preliminary report of the result appeared in \cite{korovin02unif}}
}

@inproceedings{zhang05cade,
  author = {Ting Zhang and Henny Sipma and Zohar Manna},
  title = {The Decidability of the First-order Theory of {K}nuth-{B}endix
                 Order},
  crossref = {cade05},
  url = {http://theory.stanford.edu/\home{sipma}/papers/cade05.html},
  pages = {131--148}
}

@proceedings{cade05,
  booktitle = {20th International Conference on Automated Deduction},
  title = {20th International Conference on Automated Deduction},
  editor = {Robert Nieuwenhuis},
  address = {Tallinn, Estonia},
  month = jul,
  year = 2005,
  publisher = springer,
  series = lncs,
  volume = 3632
}

@proceedings{fsttcs02,
  booktitle = {Foundations of Software Technology and Theoretical Computer Science},
  title = {Foundations of Software Technology and Theoretical Computer Science},
  address = {Kanpur, India},
  publisher = springer,
  series = lncs,
  month = dec,
  year = 2002
}

@proceedings{icalp01,
  editor = {Fernando Orejas and Paul G. Spirakis and Jan van Leeuwen},
  title = {28th International Colloquium on Automata, Languages and Programming},
  booktitle = {28th International Colloquium on Automata, Languages and Programming},
  publisher = springer,
  series = lncs,
  volume = {2076},
  year = {2001},
  isbn = {3-540-42287-0},
  month = jul,
  address = {Crete, Greece}
}

@proceedings{lics00,
  booktitle = {15th Annual {IEEE} Symposium on Logic in Computer Science},
  title = {15th Annual {IEEE} Symposium on Logic in Computer Science},
  year = 2000,
  month = jun,
  address = {Santa Barbara, CA, USA},
  organization = ieee
}

@proceedings{unif02,
  editor = {Christophe Ringeissen and Cesare Tinelli and Ralf Treinen
            and Rakesh M. Verma},
  booktitle = {Proceedings of the 16th International Workshop on Unification ({UNIF 2002)}},
  title = {Proceedings of the 16th International Workshop on Unification ({UNIF 2002)}},
  series = {Technical Report 02-05, } # deptcsiowa,
  month = jul,
  year = 2002,
  address = {Copenhagen, Denmark}
}