Abstract

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 presented.

BibTeX

@inproceedings{NHAM-IJCAR10,
  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
}