Eighteenth Annual IEEE Symposium on

Logic in Computer Science (LICS 2003)

Paper: Orienting Equalities with the Knuth-Bendix Order (at LICS 2003)

Authors: Konstantin Korovin Andrei Voronkov

Abstract

Orientability of systems of equalities is the following problem: given a system of equalities s \simeq t,..., \simeq t, does there exist a simplification ordering \succ which orients the system, that is for every i \in {1,..., n}, either s \succ t or t \succ s. This problem can be used in rewriting for finding a canonical rewrite system for a system of equalities and in theorem proving for adjusting simplification orderings during completion. We prove that (rather surprisingly) the problem can be solved in polynomial time when we restrict ourselves to the Knuth-Bendix orderings.

BibTeX

  @InProceedings{KorovinVoronkov-OrientingEqualities,
    author = 	 {Konstantin Korovin and Andrei Voronkov},
    title = 	 {Orienting Equalities with the Knuth-Bendix Order},
    booktitle =  {Proceedings of the Eighteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2003},
    year =	 2003,
    editor =	 {Phokion G. Kolaitis},
    month =	 {June}, 
    pages =      {75--},
    location =   {Ottawa, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }