cl-banner

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.

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.

 

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

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