Decreasing Diagrams and Relative Termination

TL;DR

This paper applies decreasing diagrams to prove confluence of left-linear term rewrite systems using relative termination, and encodes heuristics as SAT problems, supported by experimental results.

Contribution

It introduces a novel application of decreasing diagrams for confluence proofs and encodes heuristics as SAT problems, with experimental validation.

Findings

Confluence of left-linear systems can be established via critical pair joinability and relative termination.

Rule-labeling heuristics can be encoded as SAT problems for automated analysis.

Experimental results demonstrate effectiveness of the proposed methods.

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.