Paper: A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering (at LICS 2000)

Authors: Konstantin Korovin Andrei Voronkov

Abstract

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 Symposium on Logic in Computer Science (LICS 2000)},
    year =	 {2000},
    month =	 {June}, 
    pages =      {291--302},
    location =   {Santa Barbara, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }