Konstantin Korovin, Andrei Voronkov. A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering. In LICS. pages 291-302, 2000. [doi]
@inproceedings{KorovinV00,
title = {A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering},
author = {Konstantin Korovin and Andrei Voronkov},
year = {2000},
url = {http://www.computer.org/proceedings/lics/0725/07250291abs.htm},
tags = { algebra},
researchr = {https://researchr.org/publication/KorovinV00},
cites = {0},
citedby = {0},
pages = {291-302},
booktitle = {LICS},
}