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.


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


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 ./ <file>
  • Input systems are available at the Confluence Problems database (Cops).


For any questions or feedback please contact Julian Nagele. 

Nach oben scrollen