@inproceedings{BeckerCADE2017,
TITLE = {A Transfinite {K}nuth--{B}endix Order for Lambda-Free Higher-Order Terms},
AUTHOR = {Becker, Heiko and Blanchette, Jasmin Christian and Waldmann, Uwe and Wand, Daniel},
LANGUAGE = {eng},
ISBN = {978-3-319-63045-8},
DOI = {10.1007/978-3-319-63046-5_27},
PUBLISHER = {Springer},
YEAR = {2017},
DATE = {2017},
BOOKTITLE = {Automated Deduction -- CADE 26},
EDITOR = {de Moura, Leonardo},
PAGES = {432--453},
SERIES = {Lecture Notes in Artificial Intelligence},
VOLUME = {10395},
ADDRESS = {Gothenburg, Sweden},
}