CSI: New Evidence – A Progress Report

Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp

Proceedings of the 26th International Conference on Automated Deduction (CADE-26), Lecture Notes in Artificial Intelligence 10395, pp. 385 – 397, 2017.


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.


  PDF |    doi:10.1007/978-3-319-63046-5_24  


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"
Nach oben scrollen