cl-banner

CSIlgplv3_logo


Description

CSI is an automatic confluence prover for first-order rewrite systems. An extension to higher-order pattern rewrite systems is described here.

News
  • June 2020: Version 1.2.4 released. (CoCo 2020 version; adds upside-parallel-closure criterion)
  • April 2019: Version 1.2.3 released. (CoCo 2019 version; adds UNC for shallow systems)
  • December 2018: Version 1.2.2 released. (right-reducibility for NFP; improved SRS support for CR)
  • June 2018: Version 1.2.1 released. (CoCo 2018 version; adds UNC for linear shallow systems)
  • January 2018: Version 1.2 released. (adds certification for persistent decomposition).
  • September 2017: Version 1.1 released. (CoCo 2017).
  • June 2017: Version 1.0.1 released. (improved UNR check for ground TRSs).
  • February 2017: Version 1.0 released (experiments).
  • September 2016: Version 0.6 released (CoCo 2016).
  • July 2015: Version 0.5.1 released (CoCo 2015).
  • February 2015: Version 0.5 released (certified rule labeling; removal and addition of redundant rules).
  • January 2014: Version 0.4.1 released (improved strategy for non-left-linear TRSs).
  • November 2013: Version 0.4 released (improved incremental labeling).
  • July 2013: Version 0.3 released (CoCo 2013).
  • May 2012: Version 0.2 released (CoCo 2012).
  • February 2011: Version 0.1 released (experiments).
Downloads

Use the web interface or statically linked precompiled binaries for Linux (64 bit) if you do not want to build CSI on your own.

You can also download the source. The current version is 1.2.4. To compile

  • download and extract the archive
  • follow the instructions in README
  • type make
  • type ./csi.sh <file>
Documents
Contact

The main developers are (in alphabetical order) Bertram Felgenhauer, Aart Middeldorp, Julian Nagele, and Harald Zankl. For any questions or feedback please write to csi@informatik.uibk.ac.at.

Support

The development of CSI is supported by FWF (Austrian Science Fund) projects P22467 and P27528.

Nach oben scrollen