Confluence by Critical Pair Analysis Revisited

Nao Hirokawa, Julian Nagele, Vincent van Oostrom, Michio Oyamaguchi

27th International Conference on Automated Deduction, Lecture Notes in Computer Science 11716, pp. 319 – 336, 2019.


We present two methods for proving confluence of left-linear term rewrite systems. One is hot-decreasingness, combining the parallel/development closedness theorems with rule labelling based on a terminating subsystem. The other is critical-pair-closing system, allowing to boil down the confluence problem to confluence of a special subsystem whose duplicating rules are relatively terminating.


  PDF |    doi:10.1007/978-3-030-29436-6_19  |  © Springer Nature Switzerland AG 2019


author = "Nao Hirokawa and Julian Nagele and Vincent van Oostrom and Michio Oyamaguchi",
title = "Confluence by Critical Pair Analysis Revisited",
booktitle = "Proceedings of the 27th International Conference on Automated Deduction",
editor = "Pascal Fontaine",
series = "Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence",
volume = 11716,
pages = "319-336",
year = 2019,
publisher = "Springer",
doi = ""
arxiv = ""
Nach oben scrollen