@string{conf:TPHOLs = "Theorem Proving in Higher Order Logics, TPHOLs"}
@string{conf:RTA    = "Rewriting Techniques and Applications, RTA"}
@string{conf:LPAR   = "Logic for Programming, Artificial Intelligence, and Reasoning, LPAR"}
@string{ai    = "Acta Informatica"}
@string{jar   = "Journal of Automated Reasoning"}
@string{lncs = "LNCS"}
@string{lipics = "Leibniz International Proceedings in Informatics"}


@incollection{KB70,
  author    = "Donald E. Knuth and Peter Bendix",
  title     = "Simple Word Problems in Universal Algebras",
  booktitle = "Computational Problems in Abstract Algebra",
  optpublisher = "Pergamon Press, New York",
  year      = 1970,
  opteditor    = "J. Leech",
  pages     = "263-297",
  doi = {10.1007/978-3-642-81955-1_23},
}

@article{DKM90,
  author    = "Jeremy Dick and John Kalmus and Ursula Martin",
  title     = "Automating the {K}nuth-{B}endix ordering",
  journal   = ai,
  volume    = 28,
  number    = 2,
  pages     = "95-119",
  year      = 1990,
  doi      = {10.1007/BF01237233},
}

@inproceedings{TS09b,
  author={Ren{\'e} Thiemann and Christian Sternagel},
  title={Certification of Termination Proofs using {\ceta}},
  booktitle=conf:TPHOLs # "'09",
  opteditor={Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel},
  year=2009,
  volume=5674,
  pages={452-468},
  optpublisher=pub:spr,
  series=lncs,
  doi={10.1007/978-3-642-03359-9_31}
}
  
@inproceedings{S89,
  author    = "Joachim Steinbach",
  title     = "Extensions and Comparison of Simplification Orders",
  booktitle = conf:RTA # "'89",
  series    = lncs,
  volume    = 355,
  year      = 1989,
  pages     = "434-448",
  doi      = {10.1007/3-540-51081-8_124}
}

@article{ZHM09,
 author = "Harald Zankl and Nao Hirokawa and Aart Middeldorp",
 title  = "{KBO} Orientability",
 journal= jar, 
 volume = 43,
 number = 2,
 pages  = {173-201},
 year   = 2009,
 doi   = {10.1007/s10817-009-9131-z}
}

@inproceedings{LW07,
  author    = {Michel Ludwig and Uwe Waldmann},
  title     = {An Extension of the {K}nuth--{B}endix Ordering with {LPO}-Like Properties},
  booktitle = conf:LPAR # "'07",
  year      = {2007},
  pages     = {348-362},
  series    = lncs,
  optpublisher = springer,
  volume    = {4790},
  doi      = {10.1007/978-3-540-75560-9_26},
}

@inproceedings{paper,
  author = {Christian Sternagel and René Thiemann},
  title = {Formalizing {K}nuth--{B}endix Orders and {K}nuth--{B}endix Completion},
  booktitle = conf:RTA # "'13",
  year = {2013},
  pages = {287-302},
  volume = 2,
  series = lipics,
  doi    = {10.4230/LIPIcs.RTA.2013.287},
}