cl-banner

Deciding Confluence of Ground Term Rewrite Systems in Cubic Time

Bertram Felgenhauer

Proceedings of the 23rd International Conference on Rewriting Techniques and Applications (RTA 2012), Leibniz International Proceedings in Informatics 15, pp. 165 – 175, 2012.

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.

 

  PDF |    doi:10.4230/LIPIcs.RTA.2012.165  |  © Creative Commons License – NC – ND

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
}
Nach oben scrollen