Welcome to the website of mkbTT!

mkbTT is a tool for Knuth-Bendix completion: given a set of input equalities, it tries to generate a confluent and terminating rewrite system that can be used to decide the equational theory. The tool differs from traditional tools in two respects. Firstly, instead of requiring a reduction order as input, it ensures termination of the generated rewrite system by employing modern termination tools following the approach developed by Wehrman, Stump and Westbrook [1]. This allows for a more automatic and user-friendly interface. Besides, by exploiting the full power of modern termination provers it also admits for completions that cannot be obtained with standard reduction orders. Secondly, mkbTT relies on the multi-completion approach developed by Kondo and Kurihara [2] to keep track of multiple possible orientations in parallel.

On this website you can download the tool, play around with the web interface or have a look at detailled experimental results obtained with the latest version. Previous versions may also be accessed.

Papers

More details about mkbTT and the underlying inference system are described in the following publications. The first version was presented in A more detailled report on the approach containing also proofs was submitted to a Japanese journal: Some optimizations such as critical pair criteria, isomorphisms and term indexing techniques were added in a later version:

Versions

Information about earlier versions such as the initial mkbTT 1.0 and mkbTT 2.0 described in the RTA 2010 system description are still available but the corresponding websites are no longer updated.

Contact

If you have any further questions, please contact Sarah Winkler

1	I. Wehrman, A. Stump, and E.M. Westbrook. Slothrop: Knuth-Bendix completion with a modern termination checker. In Proc. 17th RTA, volume 4098 of LNCS, pages 287-296, 2006.
2	M. Kurihara and H. Kondo. Completion for multiple reduction orderings. JAR, 23(1):25-42, 1999.