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

• A scaladoc is available for KBCV and the termlib on which KBCV depends.
• T. Sternagel, S. Winkler, and H. Zankl,
  Recording Completion for Certificates in Equational Reasoning
  In Proceedings of the 4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP 2015),
  ACM pp 41-47, 2015.
  © The Authors
• T. Sternagel and H. Zankl,
  KBCV -- Knuth-Bendix Completion Visualizer
  In Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR 2012),
  LNCS (LNAI) 7364, pp 530-536, 2012.
  © Springer-Verlag

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

• March 17 2017: KBCV and termlib are now built upon Scala version 2.11.0.
• March 15 2017: Bugfix of collapse inference rule in termlib 2.0.0.3.
• March 2 2017: KBCV on Android released.
• October 15 2014: Version 2.1.0.2 released. Featuring automatic certifiable equational logic proofs in various formats.
• April 8 2013: Full version (2.0) released. We have optimized the automatic completion procedure. Also a new version of termlib (2.0) is used.
• February 15 2013: KBCV and termlib are now built upon Scala version 2.10.0.
• December 11 2012: From 1.8.1.3 on you may issue multiple commands in text-mode by separating them with ';'.
• December 6 2012: Starting from version 1.8.0.1 there is now a changelog available.
• September 30 2012: Full version (1.8) released. This is the version described in my master thesis.
• April 3 2012: Full version (1.7) released. Automatic completion may now be limited to a fixed number of rounds. Internal state has been overhauled and many small bugs fixed.
• January 30 2012: Full version (1.6) released. We have optimized the automatic completion procedure. Also a new version of termlib (1.2) is used.
• January 16 2012: Full version (1.5) released. We have built in support for equational proof trees and certifiable xml output for the completion proof and the equational proof trees.
• August 28 2011: I have also started a scaladoc for termlib which hopefully will grow in the next weeks.
• August 26 2011: I have started a scaladoc for kbcv which hopefully will grow in the next weeks.
• August 25 2011: Now KBCV and its source code is available under the GNU Lesser General Public License. Also a scala termlib was split from KBCV for separate usage.
• November 12 2010: Full version (1.1) released.
• September 24 2010: Full version (1.0) released.
• August 19 2010: Preliminary version (0.7) released.
• July 2 2010: Preliminary version (0.6) released.

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.