License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2012.165
URN: urn:nbn:de:0030-drops-34918
URL: http://drops.dagstuhl.de/opus/volltexte/2012/3491/
Go to the corresponding Portal


Felgenhauer, Bertram

Deciding Confluence of Ground Term Rewrite Systems in Cubic Time

pdf-format:
Document 1.pdf (475 KB)


Abstract

It is well known that the confluence property of ground term rewrite systems (ground TRSs) is decidable in polynomial time. For an efficient implementation, the degree of this polynomial is of great interest. The best complexity bound in the literature is given by Comon, Godoy and Nieuwenhuis (2001), who describe an O(n^5) algorithm, where n is the size of the ground TRS. In this paper we improve this bound to O(n^3). The algorithm has been implemented in the confluence tool CSI.

BibTeX - Entry

@InProceedings{felgenhauer:LIPIcs:2012:3491,
  author =	{Bertram Felgenhauer},
  title =	{{Deciding Confluence of Ground Term Rewrite Systems in Cubic Time}},
  booktitle =	{23rd International Conference on Rewriting Techniques and Applications (RTA'12) },
  pages =	{165--175},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-38-5},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{15},
  editor =	{Ashish Tiwari},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3491},
  URN =		{urn:nbn:de:0030-drops-34918},
  doi =		{http://dx.doi.org/10.4230/LIPIcs.RTA.2012.165},
  annote =	{Keywords: confluence, ground rewrite systems, decidability, polynomial time}
}

Keywords: confluence, ground rewrite systems, decidability, polynomial time
Seminar: 23rd International Conference on Rewriting Techniques and Applications (RTA'12)
Issue Date: 2012
Date of publication: 15.05.2012


DROPS-Home | Fulltext Search | Imprint Published by LZI