• Media type: E-Article; Electronic Conference Proceeding; Text
  • Title: Deciding Confluence of Ground Term Rewrite Systems in Cubic Time
  • Contributor: Felgenhauer, Bertram [Author]
  • imprint: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2012
  • Language: English
  • DOI: https://doi.org/10.4230/LIPIcs.RTA.2012.165
  • Keywords: polynomial time ; decidability ; ground rewrite systems ; confluence
  • Origination:
  • Footnote: Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
  • Description: 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.
  • Access State: Open Access