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 Symposium on Logic in Computer Science (LICS 2002)},
    year =	 {2002},
    month =	 {July}, 
    pages =      {447--457},
    location =   {Copenhagen, Denmark}, 
    publisher =	 {IEEE Computer Society Press}
  }