2026-07-23T22:06:42Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3491 2024-03-06T10:34:17Z ddc:004 open_access

Deciding Confluence of Ground Term Rewrite Systems in Cubic Time Felgenhauer, Bertram confluence ground rewrite systems decidability polynomial time 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Bertram Felgenhauer 2012 Is Part Of LIPIcs, Volume 15, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) (2012) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2012.165 urn:nbn:de:0030-drops-34918 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2012.165 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode