CSI^ho

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).

Downloads

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>

Input systems are available at the Confluence Problems database (Cops).

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.

Contact

For any questions or feedback please contact Julian Nagele.