Abstract

Unravelings are a class of transformations of conditional term rewriting systems into unconditional systems. Such transformations have been used to analyze and simulate conditional rewrite steps by unconditional rewrite steps for properties like (operational) termination. In this paper, we show how to prove confluence of conditional term rewriting systems via unravelings.

BibTeX

@inproceedings{KGNNBG-IWC13,
  author    = "Karl Gmeiner and Naoki Nishida and Bernhard Gramlich",
  title     = "Proving Confluence of Conditional Term Rewriting Systems via
               Unravelings",
  booktitle = "Proceedings of the 2nd International Workshop on Confluence",
  editor    = "Nao Hirokawa and Vincent van Oostrom",
  pages     = "35--39",
  year      = 2013
}