Department of Computer Science

University of Innsbruck

mkbTT (2.2)

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.

Examples

Load own example

Syntax highlighting

Tool input

Completion method

Standard completion

Ordered completion

Normalized completion

Output

Completed TRS

Statistics

Proof

Certify output with CeTA