Tools on Rewriting
-
A Coq library on rewriting and termination with tactics for automatically checking the conditions of termination theorems.
-
CeTA is a tool that certifies termination analysis (in terms of a termination proof) provided by a termination tool.
Formalizing Knuth-Bendix Orders and Knuth-Bendix Completion In Proc. of the 24th International Conference on Rewriting Techniques and Applications (RTA'13), LIPIcs, to appear. * C. Ste...
-
The Tyrolean Termination Tool 2 (TTT2) is a tool for automatically proving (and disproving) termination of rewrite systems. It is the completely redesigned successor of TTT. Current (non-)termination techniques include approximated dependency graph, argument filtering, bounds, dependency pair method, Knuth-Bendix order, lexicographic path order, loop detection, matrix interpretation, polynomial interpretation, predictive labeling, recursive SCC, root labeling, semantic labeling, simple projection and subterm criterion, uncurrying, usable rules.
The current version is 1.11. Get recent versions....
-
The Tyrolean Complexity Tool (TCT) is a tool for automatically proving (low) upper bounds on the derivational complexity and runtime complexity of terminating term rewriting systems. Whereas Version 1.0 is strongly based on the automatic termination prover TTT2, Version 2.0 is rewritten from scratch in the purely functional programming language Haskell.
* Simplified configuration. See an example (available also in the source distribution) or the updated documentation...
-
Anagopos is an open source tool for visualizing reduction graphs of terms in lambda calculus and term rewriting. Anagopos allows step-by-step generation of reduction graphs under six different drawing algorithms.
-
AProVE is a system for automated termination and innermost termination proofs of term rewrite systems (TRSs). Moreover, AProVE also handles several other formalisms, e.g., logic programs (Prolog), functional programs (Haskell 98), conditional TRSs, TRSs modulo AC, context-sensitive TRSs, etc. The power of AProVE is demonstrated in the annual International Competition of Termination Tools, where AProVE was the most powerful tool for termination of TRSs in 2004, 2005, 2006, 2007, and 2008.
* Download: You can download the full version of AProVE....
-
An automatic termination of narrowing prover.
Copyright © 2013 ELP Group | Theme zBench | Powered by WordPress...
-
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.0 (source code) ... Please see included README file for instructions. ... * maxcomp_1.0-1_amd64.deb ... Installation instructions: 1. download and extract yices 1.0.34 (yices-1.0...
-
Jambox is an automated termination prover for string and term rewriting systems.
-
REPIUS (REwrite-Program Inversion and Unraveling System) is a tool that (fully or partially) inverts a constructor TRS written in a .trs file and unravels the resulting inverse CTRS. The prototype (Ver. 0.x) was developed following the approach in (Nishida et al., RTA'05) and employs a variant of Ohlebusch's unraveling transformation. The current version was wholly implemented, introducing a new approach to tail-recursive functions into the previous approach to full inversion (Nishida et al., IEICE'05). The unraveling step will be implemented as an option of postprocess of inversion, and the partial inversion approach will be also implemented as an extension. The current implementation is based on the technique in (Nishida and Vidal, RTA'11).
Updated: Jun 27, 2012 ... June 27, 2012 MSV is correct for constructor TRSs w.r.t. constructor-based reduction. ___________________________________________________________...
-
Saigawa is an automatic confluence tool for first-order term rewrite systems. It supports the next confluence criteria: Knuth and Bendix' criterion, decreasing confluence, and rule-labeling
-
ACP is an automated confluence prover for term rewriting systems (TRSs). A distinct feature of ACP is incorporation of several divide-and-conquer criteria such as those for commutative (Toyama,1988), layer-preserving (Ohlebusch,1994) and persistent (Aoto and Toyama, 1997) combinations. For a TRS to which direct confluence criteria do not apply, the prover decomposes it into components and tries to apply direct confluence criteria to each component. Then the prover combines these results to infer the (non-)confluence of the whole system.
-
CSI is an automatic confluence prover for first-order rewrite systems. It is based on the Tyrolean Termination Tool 2 (TTT2).
* May 2012: Version 0.2 released. ... You can also download the source. The current version is 0.2. To ... * type ./csi.sh <file>...
-
μ-Term is a tool which can be used to verify a number of termination properties of Term Rewriting Systems via different reduction relations which can be associated to them: termination of rewriting, termination of innermost rewriting, termination of context-sensitive rewriting, and termination of innermost context-sensitive rewriting.
rewriting and the third most powerful tool for proving termination of ... FEDER MINECO MICINN GVA UPV DSIC "Una manera de hacer Europa"...
-
Autowrite is a project carried out at the LaBRI (Laboratoire Bordelais de Recherche en Informatique) at the University of Bordeaux. Autowrite is an experimental tool written in Common Lisp for checking properties of term rewrite systems and handling bottom-up term (tree) automata. It is written in Steele Bank Common Lisp (SBCL). It was initially designed to check call-by-need (CBN) properties of TRSs. For this purpose, it also implements the main operations on term automata constructions (determinization, minimization, union, intersection, emptiness, ...) and many operations on terms. Recently, fly-automata have been added to the implementation. The transition function of a fly-automaton is a (Lisp) transition function instead of a table of transitions. Fly-automata may be used when the transition table is too big to be stored and can also be infinite in two ways (infinite signature, infinite number of states). A graphical interface interface written using FreeCLIM, the free implementation of the CLIM specification frees the user from any Lisp knowledge. From this interface, one can handle term rewrite systems, term automata and build many term automata related to TRSs and graphs represented as terms; one can check membership to call-by-need classes for the different considered approximations of a given system.
-
CaT is a powerful analyzer for the complexity of term rewrite systems. It is based on the fast and powerful termination analyzer TTT2. In 2008 and 2009, CaT won all categories in the international termination competition related to complexity in which it participated.
2010, and 2011 in the international termination competition....
-
CiME 3 is a rewriting toolbox that provides Coq certificates for termination proofs (standard rewriting) obtained using various criteria: Dependency pairs (plain/marks, graphs refinements with or without sub-term criterion), as well as various orderings (polynomial interpretations, matrix interpretations, full RPO with status, with AFS refinements).
+ Release CiME 3 binaries for i686 64 bits linux: [static](Bugfix 2011/05/26) [dynamic] (Bugfix 2011/04/01)...
-
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...
-
RAPT (Rewriting-based Automated Program Transformation system) is a program transformation system using transformation templates, which implements a framework of program transformation. RAPT transforms many-sorted TRSs according to input correct templates with verification of its correctness.
-
StreamBox: A Tool for Proving Stream Equality.
-
TrafO, Transformation of Outermost Termination, is a transformation tool for proving outermost termination.
-
A termination tool.
-
TNT, a transformation for analyzing narrowing termination, is a tool developed by German Vidal and Naoki Nishida to analyze the termination of narrowing.
-
TPA is a tool for proving termination and relative termination of term rewrite systems automatically. It is developed by Adam Koprowski at TU/e within TORPA project. TPA has some novel features compared with other termination provers. It uses the following termination proving techniques: polynomial and matrix interpretations, semantic and predictive labeling (both with booleans and with natural numbers), recursive path ordering (RPO), dependency pair transformation (DP), and dummy elimination.
-
Slothrop is an automated equational theorem prover that performs a variant of Knuth-Bendix completion.
-
By this tool proofs of (relative) termination of string rewriting systems (SRS) can be generated automatically. It was developed by Hans Zantema starting in July 2003. It is based on a combination of polynomial and matrix interpretations, recursive path order, semantic labelling, dependency pairs, transformation order, dummy elimination and RFC-match-bounds. Proofs of non-termination are found by using ancestor graphs. In both the termination competition of 2004 and the termination competition of 2005 this tool performed the best of all tools in the category of string rewriting.