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.)

Description

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.

Documentation

Download

The full version is available here. You will need to have Scala 2.11.0 installed on your system.
Usage:
tar xfz kbcv-2.1.0.6.tar.gz
cd kbcv-2.1.0.6
./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-2.1.0.6-sources.jar
termlib source code: termlib_2.11-2.0.0.4-sources.jar

Compilation

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:
kbcv/
  build.sbt
  project/
    build.properties
    assembly.sbt
  src/main/scala
    the kbcv sources
  termlib/
    src/main/scala
      the termlib sources

Old Versions

KBCV 2.1.0.5 source code: kbcv_2.11-2.1.0.5-sources.jar
KBCV 2.1.0.4 source code: kbcv_2.10-2.1.0.4-sources.jar
KBCV 2.0.0.2 source code: kbcv_2.10-2.0.0.2-sources.jar
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 2.0.0.3 source code: termlib_2.10-2.0.0.3-sources.jar
termlib 1.1 source code: termlib_2.9.1-1.1-sources.jar

Changelog

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

News

Contact

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

Contributors

We greatfully acknowledge useful comments by Christian Sternagel.

Third Party Libraries

KBCV uses termlib_2.10-2.0.0.4.jar, 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.