A Certifiable Confluence Checker for Conditional Term Rewrite Systems

ConCon is a fully automatic confluence checker for oriented first-order conditional term rewrite systems (CTRSs). It is written in Scala and available under the LGPL license. For some of its methods ConCon issues calls to the external unconditional confluence and termination checkers CSI and TTT2 as well as the maximal completion tool MaedMax. ConCon first tries to simplify rules and remove infeasible rules from the input system, then it employs the following three confluence criteria:

• (A) a quasi-decreasing strongly deterministic 3-CTRS is confluent if all its critical pairs are joinable [ALS94],
• (B) an almost orthogonal extended properly oriented right-stable 3-CTRS is confluent [SMI95],
• (C) a deterministic 3-CTRS R is confluent if its unraveling U(R) is left-linear and confluent [WT15].

In parallel ConCon also tries to show non-confluence using conditional narrowing (and some other heuristics). To make criteria (A) and (B) more useful, ConCon uses a variety of methods to check for infeasibility [SM15] of conditional critical pairs, ranging from a simple technique based on unification, via symbol transition graph analysis, reachability problem decomposition, the exploitation of certain equalities in the conditions, and tree automata completion to equational reasoning. ConCon can generate certifiable output for all implemented methods [SS16, SS17, SS17b, SW19, WT15]. This output can be certified by CeTA. The current version of ConCon is 1.10.1.0.

News

• 01.08.2021: ConCon 1.10.1.0 bugfix release
• 05.07.2020: ConCon 1.10.0.0 released (winner of CPF-CTRS and CTRS categories and 2nd place in INF category in CoCo'20)
• 08.04.2019: ConCon 1.9.1.0 bugfix release
• 14.03.2019: ConCon 1.9.0.0 released (winner of CPF-CTRS category in CoCo'19)
• 25.02.2019: ConCon 1.8.0.0 released
• 11.11.2018: ConCon 1.7.2.0 released
• 02.10.2018: ConCon 1.6.2.0 released
• 21.08.2018: ConCon 1.5.2.0 released
• 08.11.2017: ConCon 1.5.1.0 released
• 01.08.2017: ConCon 1.5.0.0 released (winner of CTRS category in CoCo'17 and CoCo'18)
• 14.02.2017: ConCon 1.4.0.0 officially released
• 12.09.2016: ConCon 1.3.2.0 officially released
• 08.09.2016: ConCon 1.3.2.0 wins first prize at CoCo'16
• 02.05.2016: ConCon 1.3.1.0 released
• 02.08.2015: ConCon 1.3.0.0 wins first prize at CoCo'15
• 13.07.2014: ConCon 1.2.0.3 wins first prize at CoCo'14

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.10.1.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.13-1.10.1.0-sources.jar

Old Versions

ConCon 1.10.0.0 (sources)
ConCon 1.9.1.0 (sources)
ConCon 1.9.0.0 (sources)
ConCon 1.8.0.0 (sources)
ConCon 1.7.2.0 (sources)
ConCon 1.6.2.0 (sources)
ConCon 1.5.2.0 (sources)
ConCon 1.5.1.0 (sources)
ConCon 1.5.0.0 (sources)
ConCon 1.4.0.0 (sources)
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

For general questions to the developer send a mail to concon@informatik.uibk.ac.at.