Document Open Access Logo

Deciding Confluence of Ground Term Rewrite Systems in Cubic Time

Author Bertram Felgenhauer

PDF

File

Thumbnail PDF
PDF
LIPIcs.RTA.2012.165.pdf
  • Filesize: 475 kB
  • 11 pages

Document Identifiers

Subject Classification

Keywords
  • confluence
  • ground rewrite systems
  • decidability
  • polynomial time

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get BibTex

Bertram Felgenhauer. Deciding Confluence of Ground Term Rewrite Systems in Cubic Time. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 15, pp. 165-175, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012) https://doi.org/10.4230/LIPIcs.RTA.2012.165

Author Details

Bertram Felgenhauer
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact