Abstract

Rule labeling is a heuristic, suggested by van Oostrom, for applying decreasing diagrams to linear TRSs. The heuristic also works for left-linear TRSs under certain relative termination conditions. In this note we apply the rule labeling heuristic to arbitrary left-linear TRSs, based on considering parallel reduction relations and parallel critical peaks.

BibTeX

@inproceedings{BF-IWC13,
  author    = "Bertram Felgenhauer",
  title     = "Rule Labeling for Confluence of Left-Linear Term Rewrite
               Systems",
  booktitle = "Proceedings of the 2nd International Workshop on Confluence",
  editor    = "Nao Hirokawa and Vincent van Oostrom",
  pages     = "23--27",
  year      = 2013
}