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.
pdf 
doi:10.1007/978-3-030-29436-6_19
Springer Nature Switzerland AG 2019
Abstract
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.
BibTex
@inproceedings{NHJNVvOMO-CADE27, 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 = "https://doi.org/10.1007/978-3-030-29436-6_19" arxiv = "https://arxiv.org/abs/1905.11733v2"}