Abstract

This paper describes the automatic mode of the new version of the Knuth-Bendix Completion Visualizer. The internally used data structures have been overhauled and the performance was dramatically improved by introducing caching, parallelization, and term-indexing in the computation of critical pairs and simplification. The new version is much faster and can complete three more systems.

BibTeX

@inproceedings{TS-IWC13,
  author    = "Thomas Sternagel",
  title     = "KBCV 2.0 -- Automatic Completion Experiments",
  booktitle = "Proceedings of the 2nd International Workshop on Confluence",
  editor    = "Nao Hirokawa and Vincent van Oostrom",
  pages     = "53--57",
  year      = 2013
}