The Conditional Confluence Tool

ConCon is a fully automatic confluence checker for oriented first-order conditional term rewrite systems (CTRSs). The tool implements three known confluence criteria: Several techniques to check infeasibility of conditional critical pairs are used, making criteria (A) and (B) more useful. Also some simple techniques to detect non-confluence are implemented. For some of the methods ConCon issues calls to the external unconditional confluence and termination checkers CSI and TTT2. Nearly all methods used in ConCon are now certifiable by CeTA. ConCon is written in Scala 2.12 and available under the LGPL license. The current version of ConCon is 1.4.0.0.

News

Download

The full version is available here (~12M).

Usage

You only need to have a Java JDK8 installed on your system, then by typing
java -jar concon-1.4.0.0.jar
in a terminal you start ConCon. The Scala sources are prepacked in the ConCon jar. You may adjust the paths and flags of your external unconditional confluence and termination checkers by putting a file called concon.ini in the same location as your ConCon jar. This file may look like the following concon.ini.
You can also use the web-interface online.

Source Code

ConCon source code: concon_2.12-1.4.0.0-sources.jar

Old Versions

ConCon 1.3.2.0 (sources)
ConCon 1.3.1.0 (sources)
ConCon 1.3.0.0 (sources)
ConCon 1.2.0.3 (sources)
ConCon 1.2.0.0 (sources)
ConCon 1.1.0.0 (sources)

Contact

The author is Thomas (dot) Sternagel [at] uibk (dot) ac (dot) at.