Knuth-Bendix Completion Visualizer

KBCV on Android

Check out the new Android app of KBCV by Christina Kohl:
+ new + kbcv.apk + new + (last updated: 27.09.2017)
You can directly download and install it on your Android device.
(Provided you allow to install from unknown sources in the security settings of your device.)


The Knuth-Bendix Completion Visualizer (KBCV) is a tool that allows the user to interactively perform the Knuth-Bendix completion procedure. Besides, KBCV also offers a fully automatic mode. Furthermore the tool has been extended with recording completion which can be used to generate equational logic proof trees automatically. The completion proof and the generated proof trees are available in CPF, a certifiable XML format for rewriting proofs.



The full version is available here. You will need to have Scala 2.11.0 installed on your system.
tar xfz kbcv-
cd kbcv-
Hint: If you want to put the process in the background use the -g flag:
./kbcv -g &
A bundled version which comes with TTT2, MiniSmt and the needed scala libraries included is also available here.
You can also use a java web start version of the tool online here.

Source Code

KBCV source code: kbcv_2.11-
termlib source code: termlib_2.11-


To build KBCV we use the scala build tool (sbt). You should have a folder containing a src/ subfolder which contains the kbcv sources, a subfolder termlib/ also containing a src/ subfolder containing the termlib sources, and a project/ subfolder containing the following configuration files for sbt sbt-conf.tar (please unpack). So the directory tree should look as follows:
    the kbcv sources
      the termlib sources

Old Versions

KBCV source code: kbcv_2.11-
KBCV source code: kbcv_2.10-
KBCV source code: kbcv_2.10-
KBCV 1.8 source code: kbcv_2.9.1-1.8-sources.jar
KBCV 1.7 source code: kbcv_2.9.1-1.7-sources.jar
KBCV 1.6 source code: kbcv_2.9.1-1.6-sources.jar
KBCV 1.5 source code: kbcv_2.9.1-1.5-sources.jar
termlib source code: termlib_2.10-
termlib 1.1 source code: termlib_2.9.1-1.1-sources.jar


Here you find the changelog for the current KBCV and termlib.



Please direct comments, bug reports, feature requests, etc. to To report bugs please attach the log command (File → Export Command Log).


We greatfully acknowledge useful comments by Christian Sternagel.

Third Party Libraries

KBCV uses termlib_2.10-, a term library for scala maintained by Christian Sternagel and Thomas Sternagel.
KBCV is compatible with the termination tool TTT2.
KBCV generates proofs which are certifiable with CeTA.
KBCV calls the SMT solver MiniSmt to find counter models.