2019/05/28 by Nao Hirokawa, Hirokawa, Nao, Julian Nagele +5
Computer Science · #Logic, programming, and type systems #Formal Methods in Verification #Software Engineering Research
paper · pdf · doi:10.48550/arxiv.1905.11733
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.