CoLL

About

CoLL is an automatic confluence tool for left-linear term rewrite systems based on Hindley's Commutation Theorem.
The latest version is based on the techniques:

Download

The source code is freely available.

Requirement

The tools require Linux environments and OCaml. For more detailed information, see the README file bundled with the source codes.

Usage

A typical usage is
$ coll [option] <filename.trs>
Here the input file is specified in the WST competition format. The tool outputs YES if confluence is proved, NO if confluence is disproved, and MAYBE if the tool does not reach any conclusion.

Experimental Data

Experiments for Kiraku Shintani and Nao Hirokawa, ``CoLL: A Confluence Tool for Left-Linear TRSs'' (submitted). The submission is based on CoLL v1.0.
errata in Figure 1
YES of 'development closed'23 → 17
YES of 'all three ' 131 → 125
NO of 'all with elimination'8 → 9

Tool Authors

Contact