KBCV – Knuth-Bendix Completion Visualizer

Thomas Sternagel and Harald Zankl

Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR 2012), Lecture Notes in Artificial Intelligence 7364, pp. 530 – 536, 2012.


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.


  PDF |    doi:10.1007/978-3-642-31365-3_41  |  © Springer


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
Nach oben scrollen