Abstract

This paper describes a tool for Knuth-Bendix completion. In its interactive
mode the user only has to select the orientation of equations into rewrite
rules; all other computations (including necessary termination checks) are
performed internally. Apart from the interactive mode, the tool also
provides a fully automatic mode. Moreover, the generation of (dis)proofs in
equational logic is supported. Finally, the tool outputs proofs in a
certifiable format.

BibTeX

inproceedings{TSHZ-IJCAR12,
  author      = "Thomas Sternagel and Harald Zankl",
  title       = "{KBCV} - {Knuth-Bendix} Completion Visualizer",
  booktitle   = "Proceedings of the 6th International Joint Conference on
                 Automated Reasoning",
  series      = "Lecture Notes in Artificial Intelligence",
  volume      = 7364,
  pages       = "530--536",
  publisher   = "Springer-Verlag",
  year        = 2012
}