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 Entry

@article{HM-JAR11,
 author    = "Nao Hirokawa and Aart Middeldorp",
 title     = "Decreasing Diagrams and Relative Termination",
 journal   = "Journal of Automated Reasoning",
 volume    = 47,
 number    = 4,
 pages     = "481--501",
 year      = 2011,
 doi       = "10.1007/s10817-011-9238-x"
}