A Reliable 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 theorem prover Waldmeister. ConCon first tries to simplify rules and remove infeasible rules from the input system, then it employs the following three confluence criteria: 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, WT15] except the infeasibility check employing equational reasoning via Waldmeister. This output can be certified by CeTA. The current version of ConCon is 1.5.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.5.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.5.0.0-sources.jar

Old Versions

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.