CSI^ho

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

Download

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.1. To compile

Input systems are available at the Confluence Problems database (Cops).

Documents

Contact

For any questions or feedback please contact Julian Nagele.