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

Contact

For any questions or feedback please contact Julian Nagele.