Tools on Rewriting

4 tools found.

• Slothrop

  last modified: Dec 03, 2023 12:57:32

  

  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...

  categories completion_tool completion term_rewriting

• mkbTT

  last modified: Mar 06, 2019 15:14:00

  

  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...

  categories completion_tool completion term_rewriting

• Maxcomp

  last modified: Mar 09, 2015 19:41:15

  

  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...

  categories completion_tool completion term_rewriting

• mascott

  last modified: Aug 24, 2012 17:14:03

  

  mascott is a fully automatic AC-completion tool.

  categories completion_tool completion AC-completion term_rewriting