Confluence by Critical Pair Analysis Revisited (Extended Version)
Logic in Computer Science
2019-06-04 v2 Symbolic Computation
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.
Cite
@article{arxiv.1905.11733,
title = {Confluence by Critical Pair Analysis Revisited (Extended Version)},
author = {Nao Hirokawa and Julian Nagele and Vincent van Oostrom and Michio Oyamaguchi},
journal= {arXiv preprint arXiv:1905.11733},
year = {2019}
}
Comments
Added a reference to the conference version