Lics

IEEE Symposium on Logic in Computer Science

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

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}
 }