Decreasing Diagrams and Relative Termination

Nao Hirokawa and Aart Middeldorp

Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010), Lecture Notes in Artificial Intelligence 6173, pp. 487 – 501, 2010.


In this paper we use the decreasing diagrams technique to show that a left-linear term rewrite system R is confluent if all its critical pairs are joinable and 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 present-ed.


  PDF |    doi:10.1007/978-3-642-14203-1_41  |  © Springer


author = "Nao Hirokawa and Aart Middeldorp",
title = "Decreasing Diagrams and Relative Termination",
booktitle = "Proceedings of the 5th International Joint Conference on Automated Reasoning",
series = "Lecture Notes in Artificial Intelligence",
volume = 6173,
pages = "487--501",
publisher = "Springer-Verlag",
year = 2010
Nach oben scrollen