Abstract

Logically Constrained Term Rewriting Systems (LCTRSs) provide a general framework for term rewriting with constraints. We discuss a simple dependency pair approach to prove termination of LCTRSs. We see that existing techniques transfer to the constrained setting in a natural way.

BibTeX

@inproceedings{CK-WST13,
  author    = "Cynthia Kop",
  title     = "Termination of {LCTRSs}",
  booktitle = "Proceedings of the 13th International Workshop on
               Termination (WST 2013)",
  pages     = "59--63",
  year      = "2013"
}