Tools on Rewriting
-
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...
-
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...
-
MiniSmt is a simple SMT solver for non-linear arithmetic based on MiniSat and Yices. It accepts the SMT-LIB format as input, is efficient on small domains, supports reasoning about non-rational real numbers, and is able to output models.
The current stable version is 0.66. Get recent versions and view the...
-
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)....
-
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-...
-
The SToUT (Symbolic Computation Techniques for Unranked Terms) project provides a library for unification and anti-unification algorithms: unification with sequence variables, context sequence matching, rigid anti-unification for unranked terms and hedges, unranked second-order anti-unification, higher-order anti-unification, nominal anti-unification.