SRS Standard

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

Syntax & Semantic

The syntax and the semantics of string rewrite systems are described here. Strings are terms where every function symbol has arity 1, i.e., exactly one argument.

Formally, a string rewrite system R = {l₁ → r₁,...,l_n → r_n} is a finite set of rewrite rules.

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

Problem

Input: A string 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).