Seventeenth Annual IEEE Symposium on

Logic in Computer Science (LICS 2002)

Paper: Deciding Confluence of Certain Term Rewriting Systems in Polynomial Time (at LICS 2002)

Authors: Ashish Tiwari

Abstract

We present a polynomial time algorithm for deciding confluence of ground term rewrite systems. We generalize the decision procedure to get a polynomial time algorithm for deciding confluence of left-linear right-ground term rewrite systems. These two problems have been open for a long time and only recently the first result was independently announced in \cite{ComonGodoyNieuwenhuis01:FOCS}. Our decision procedure is based on the concepts of abstract congruence closure \cite{BachmairTiwari00:CADE} and abstract rewrite closure \cite{Tiwari01:FSTTCS}.

BibTeX

  @InProceedings{Tiwari-DecidingConfluenceo,
    author = 	 {Ashish Tiwari},
    title = 	 {Deciding Confluence of Certain Term Rewriting Systems in Polynomial Time},
    booktitle =  {Proceedings of the Seventeenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2002},
    year =	 2002,
    editor =	 {Gordon Plotkin},
    month =	 {July}, 
    location =   {Copenhagen, Denmark}, 
    publisher =	 {IEEE Computer Society Press}
  }