TRS Standard

The TRS Standard category is concerned with the question "Will every possible sequence of rewrites eventually stop?". In other words, does every computation defined by the rewrite rules eventually reach a normal form (a term where no rule applies)?

Syntax & Semantic

The syntax and the semantics of term rewrite systems are described here.

Formally, a term rewrite system R = {l₁ → r₁,...,l_n → r_n} is a finite set of rewrite rules, see [1].

A term rewrite system R is terminating if there exists no infinite rewrite sequence s₀ →_R s₁ →_R s₁ →_R ...

Problem

Input: A term rewrite system R.

Question: Does R terminate?

Possible Outputs:

• "YES" followed by a termination proof, e.g., a ranking function proving termination of R.
• "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence.
• "MAYBE" (indicating that the solver cannot prove termination).

References

• [1] Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.