Paper: A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering (at LICS 2000)
Authors: Konstantin Korovin Andrei VoronkovAbstract
We show the decidability of the existential theory of term algebras with any Knuth-Bendix ordering by giving a procedure for solving Knuth-Bendix ordering constraints.
BibTeX
@InProceedings{KorovinVoronkov-ADecisionProceduref, author = {Konstantin Korovin and Andrei Voronkov}, title = {A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering}, booktitle = {Proceedings of the Fifteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2000}, year = 2000, editor = {Martin Abadi}, month = {June}, pages = {291--302}, location = {Santa Barbara, CA, USA}, publisher = {IEEE Computer Society Press} }