Tools on Rewriting
-
CeTA is a tool that certifies termination analysis (in terms of a termination proof) provided by a termination tool.
The current version is 3.0.1. To access previous versions of CeTA and see the differences please visit this site....
-
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?...
-
μ-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.
relations which can be associated to them: ... * operational termination of conditional rewriting. ... remarkable that in the last termination competition (2021), MU-TERM ... Union Europea [2011-W...
-
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...
-
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.
-
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.
-
A termination tool for C programs.
-
THOR is an automatic tool for proving Termination of Higher-Order Rewriting. It ranked first in the last International Termination Competition (termComp) in the Higher-Order category.
Rewriting. It ranked first in the 2010 International Termination...
-
TERMPTATION (TERMination Proof Techniques automATION) is a fully automated system for proving termination (and innermost termination) of term rewrite systems (developed by C. Borralleras and A. Rubio).
Rewriting. It ranked first in the 2010 International Termination...
-
Jambox is an automated termination prover for string and term rewriting systems.
* Info + Contact + Teaching...
-
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).
-
This tool proves non-termination of string rewriting, by searching for patterns in derivations and can handle non-looping non-termination.
Apache/2.2.16 (Debian) Server at dfa.imn.htwk-leipzig.de Port 80...
-
TrafO, Transformation of Outermost Termination, is a transformation tool for proving outermost termination.
-
An analyzer for Java programs.
-
A termination tool.
-
A termination tool for logic programming.
Polytool: Proving Termination Automatically based on Polynomial Interpretations ... For Logic Programming (LP), termination analysis is done by mapping terms and atoms to a well-...
-
Vienna Modular Termination Laboratory (VMTL) is a tool for the (semi-)automatic termination analysis of rewriting systems. Currently, standard as well as context-sensitive and conditional term rewriting systems are supported. VMTL is an implementation of the dependency pair framework, in which termination of rewrite systems is analyzed by so called dependency pair processors. The search for termination proofs in VMTL is guided by a user configurable strategy featuring hierarchical grouping of processors, time-limits on the level of processor groups as well as single processors and parallelization. In addition VMTL provides open interfaces allowing to add new dependency pair processors as well as transformations/preprocessings of rewrite systems in a modular fashion.