cl-banner

CSI^holgplv3_logo


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)


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. 

Nach oben scrollen