@inProceedings{Zhang+Sipma+Manna/05/Decidability,
    author = "Ting Zhang and Henny B. Sipma and Zohar Manna",
    title = "The Decidability of the First-order Theory of
                    Term Algebras with {Knuth-Bendix} Order",
    booktitle = "the $20^{th}$ International Conference on
                     Automated Deduction (CADE'05)",
    editor = "Robert Nieuwenhuis",
    pages = "131-148",
    series = lncs,
    year = "2005",
    volume = "3632",
    publisher = "Springer-Verlag",
}