Description
CSI^ho is an automatic confluence prover for higher-order rewrite systems, specifically pattern rewrite systems as introduced by Nipkow. It is based on CSI, a confluence prover for first-order term rewrite systems.News
- July 2018: Version 0.3.2 released (CoCo 2018).
- September 2017: CSI^ho won the higher-order track at CoCo 2017.
- August 2017: Version 0.3.1 released (CoCo 2017).
- February 2017: Version 0.3 released (experiments).
- September 2016: CSI^ho won the higher-order track at CoCo 2016.
- September 2016: Version 0.2 released (CoCo 2016).
- August 2015: Version 0.1.1 released.
- August 2015: CSI^ho won the higher-order track at CoCo 2015.
- July 2015: Version 0.1 released (CoCo 2015).
Download
Use the
web interface
or a statically linked, precompiled binary for Linux
(64 bit), if you do not want
to build CSI^ho on your own.
If you do, you can also download the source. The current version is 0.3.2. To compile
- download and extract the archive
- follow the instructions in README
- type
make - type
./csiho.sh <file>
Documents
- Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp
CSI: New Evidence – A Progress Report
Proc. 26th International Conference on Automated Deduction,
Lecture Notes in Artificial Intelligence 10395, pp. 385 – 397, 2017. - Julian Nagele
CoCo 2016 Participant: CSI^ho 0.2
Proc. 5th International Workshop on Confluence,
p. 85, 2016. - Julian Nagele
CoCo 2015 Participant: CSI^ho 0.1
Proc. 4th International Workshop on Confluence,
p. 47, 2015.