KBCV - Knuth Bendix Completion Visualizer

In the experiments for completion we considered the 115 systems from the MKBTT collection. The details are available here.

KBCV 1.6 performs the recall phase while KBCV 1.7 uses auxiliary equations. Times only indicate how long it took to complete the system, the time for generating certificates is not shown.

Note: With Konqueror the xslt transformations (to display problems and proofs nicely) may not work properly.