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 Entry

@inproceedings{SM-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"
}