Abstract

This paper describes the Conditional Confluence tool, a fully automatic confluence checker for first-order conditional term rewrite systems. The tool implements various confluence criteria that have been proposed in the literature. A simple technique is presented to test conditional critical pairs for infeasibility, which makes conditional confluence criteria more useful. Detailed experimental data is presented.

BibTeX

@inproceedings{TSAM-RTATLCA14,
  author    = "Thomas Sternagel and Aart Middeldorp",
  title     = "Conditional Confluence (System Description)",
  booktitle = "Proceedings of the Joint 25th International Conference on
               Rewriting Techniques and Applications and 12th
               International Conference on Typed Lambda Calculi and
               Applications",
  editor    = "Gilles Dowek",
  series    = "Lecture Notes in Computer Science (Advanced Research in
               Computing and Software Science)",
  volume    = 8560,
  pages     = "456--465",
  year      = 2014,
  doi       = "10.1007/978-3-319-08918-8_31"
}