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



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


You only need to have a Java JDK8 installed on your system, then by typing
java -jar concon-
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-

Old Versions

ConCon (sources)
ConCon (sources)
ConCon (sources)
ConCon (sources)
ConCon (sources)
ConCon (sources)


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