License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
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://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3491/
Go to the corresponding LIPIcs Volume Portal

Felgenhauer, Bertram

Deciding Confluence of Ground Term Rewrite Systems in Cubic Time

pdf-format:
14.pdf (0.5 MB)

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 =		{10.4230/LIPIcs.RTA.2012.165},
  annote =	{Keywords: confluence, ground rewrite systems, decidability, polynomial time}
}

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

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI