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

@inproceedings{BF-RTA12,
  author    = "Bertram Felgenhauer",
  title     = "Deciding Confluence of Ground Term Rewrite Systems in
               Cubic Time",
  booktitle = "Proceedings of the 23rd International Conference on Rewriting
               Techniques and Applications",
  series    = "Leibniz International Proceedings in Informatics",
  volume    = 15,
  pages     = "165--175",
  year      = 2012
}