Tools on Rewriting
-
mkbTT is a tool for performing Knuth-Bendix completion with automatic termination tools. It is based on two ingredients: (1) the inference system for completion with multiple reduction orderings introduced by Kurihara and Kondo (1999) and (2) the inference system for completion with external termination provers proposed by Wehrman, Stump and Westbrook (2006). The tool can be used with any termination tool that satisfies certain minimal requirements.
Home Download Usage Web Interface Experiments mkbTT papers versions contact ... mkbTT is a tool for Knuth-Bendix completion: given a set of input equalities, it tries to generate a confluent and...
-
Slothrop is an automated equational theorem prover that performs a variant of Knuth-Bendix completion.
DCS, a pure functional language where termination of all functions is enforced by typing. Subtyping plays a crucial role. ... Cedille, a proof assistant based on a minimalistic impredicative const...