Decreasing Diagrams and Relative Termination

Nao Hirokawa and Aart Middeldorp

Journal of Automated Reasoning 47(4), pp. 481 – 501, 2011.


In this article we use the decreasing diagrams technique to show that a left-linear and locally confluent term rewrite system R is confluent if the critical pair steps are relatively terminating with respect to R. We further show how to encode the rule-labeling heuristic for decreasing diagrams as a satisfiability problem. Experimental data for both methods are presented.


  PDF |    doi:10.1007/s10817-011-9238-x  |  © 2011, Springer Science + Business Media B.V.


author = "Nao Hirokawa and Aart Middeldorp",
title = "Decreasing Diagrams and Relative Termination",
booktitle = "Journal of Automated Reasoning",
volume = 47,
number = 4,
pages = "481--501",
year = 2011
Nach oben scrollen