Abstract

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.

BibTeX

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