Home TRS.Tool TPDB Format Benchmark Batch Test About

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.

The tool provides the following basic functionalities:

• Determine the basic structure and syntactic properties of a given term rewriting system.
• Compute the critical pairs of the term rewriting system and determine its orthogonality, local confluence (via convergence of critical pairs) and confluence.
• Compute rewriting sequences for a given input term and term rewriting system.

It also provides a very basic analysis of some simple non-termination (via loop search).