Abstract

CSI is a strong automated confluence prover for rewrite systems which has been in development since 2010. In this paper we report on recent extensions that make CSI more powerful, secure, and useful. These extensions include improved confluence criteria but also support for uniqueness of normal forms. Most of the implemented techniques produce machine-readable proof output that can be independently verified by an external tool, thus increasing the trust in CSI. We also report on CSI^ho, a tool built on the same framework and similar ideas as CSI that automatically checks confluence of higher-order rewrite systems.

BibTeX

@inproceedings{JNBFAM-CADE17,
 author    = "Julian Nagele and Bertram Felgenhauer and Aart Middeldorp",
 title     = "{CSI}: New Evidence --- A Progress Report",
 booktitle = "Proceedings of the 26th International Conference on
              Automated Deduction (CADE-26)",
 editor    = "Leonardo de Moura",
 series    = "Lecture Notes in Artificial Intelligence",
 volume    = 10395,
 pages     = "385--397",
 year      = 2017,
 doi       = "10.1007/978-3-319-63046-5_24"
}