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 Entry

@inproceedings{HM-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",
 year      = 2010,
 doi       = "10.1007/978-3-642-14203-1\_41"
}