Tools on Rewriting
-
μ-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.
#MU-TERM » Feed MU-TERM » Comments Feed JSON oEmbed (JSON) ... DSIC VRAIN...
-
CeTA is a tool that certifies termination analysis (in terms of a termination proof) provided by a termination tool.
* 2024/06/28: IsaFoR/CeTA version 3.2 has been released. ... The current version is 3.2. To access previous versions of CeTA and see...
-
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...
-
An automatic termination of narrowing prover.
Copyright © 2023 Narradar | Powered by zBench and WordPress...
-
TNT, a transformation for analyzing narrowing termination, is a tool developed by German Vidal and Naoki Nishida to analyze the termination of narrowing.
(_) Nothing (_) labeling? (_) deletion of non-reachable rules?...
-
CSI is an automatic confluence prover for first-order rewrite systems. It is based on the Tyrolean Termination Tool 2 (TTT2).
* July 2021: Version 1.2.5 released. (CoCo 2021 version; adds outside-closure criterion) ... You can also download the source. The current version is 1.2.5. To...
-
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.
* AProVE * Web Interface * Download * References * Contributors * Contact ... annual International Competition of Termination Tools and the International Competition on Software ...
-
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.
* Apr 29 2020: Version 1.20 released (maximal polynomial interpretations) ... The current version is 1.20. Get recent versions. Or directly access...
-
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.
TcT version 3.3 released 2019/05/10 __________________________________________________________________ ... Compatibility release for recent ghc version (ghc-8.6.5)....
-
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...
-
A Coq library on rewriting and termination with tactics for automatically checking the conditions of termination theorems.
CoLoR: a Coq Library on Rewriting and termination __________________________________________________________________ ... CoLoR is a library of formal mathematical definitions and proofs of theor...
-
The Nagoya Termination Tool (NaTT) is a termination prover for term rewrite systems (TRSs), which is special for: its power due to the implementation of the weighted path order (WPO), its efficiency due to the strong cooperation with external SMT solvers, and use of the DP framework for proving relative termination
The Nagoya Termination Tool (NaTT) ... NaTT [YKS14] is a termination prover for term rewrite systems (TRSs), which is special for: * its power due to the implementation of the weighted path orde...
-
TRS.Tool is a teaching-oriented tool that can be used to learn the basic notions and concepts of term rewriting. Accordingly, it gives a lot of explicit and intermediate information about signatures, terms, positions, rules, and term rewriting systems, and also about the analysis of critical pairs. We hope that this approach will be useful to get undergraduate students (and interested people) familiarized with the basic rewriting theory and then become involved in the field.
-
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: Oct 21, 2015 ... repius.jar (Jun 27, 2012)...
-
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.
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 ...
-
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.
READ-ONLY: This project has been archived. For more information see this post....
-
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.
the whole system. ACP is participating Confluence Competition (CoCo). ... Support of certificates generation For few criteria, ACP can generate certificates in CPF format, w...
-
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
* CoLL-Saigawa 1.0 released. This is a combination of CoLL 1.1 and Saigawa 1.8. This version participates in the 4th Confluence Competition (CoCo 2014) * CoLL 1.1 released. ... * CoLL-...
-
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...
-
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.
-
Jambox is an automated termination prover for string and term rewriting systems.
* Info + Contact + Teaching...
-
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, 2011, 2012, and 2013 in the international termination competition....
-
mascott is a fully automatic AC-completion tool.
-
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).
-
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.
chiba...
-
StreamBox: A Tool for Proving Stream Equality.
-
TrafO, Transformation of Outermost Termination, is a transformation tool for proving outermost termination.
-
A termination tool.