Tools on Rewriting
-
mascott is a fully automatic AC-completion tool.
-
Maxcomp is an automatic completion tool for first-order equational systems. Given an equational system, the tool outputs a corresponding complete (i.e. confluent and terminating) term rewrite system.
* Maxcomp v1.1 (March 9, 2015; support for ocamlyices 0.7.1) ... * Maxcomp v1.0...
-
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...