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"
}