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 five techniques:

Download

The source code and 64-bit Linux executable of CoLL are freely available.

Requirement

The tool requires: Please set PATH to yices.

Compilation

Type 'make'

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