CSI

Description

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

News

Download

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

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

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.