Decreasing Diagrams and Relative Termination

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.

• Type: Conference
• Year: 2010
• Where: CADE
• Authors: Nao Hirokawa, Aart Middeldorp
• Keywords: CADE 2010, Critical Pair, Critical Pair Steps, Left-linear Term Rewrite, Logical Reasoning