A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering.

Konstantin Korovin, Andrei Voronkov

Browse the full LICS paper archive.