Tools on Rewriting
-
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...
-
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.
-
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-...