TRS Standard - Revision history

JCKassing: Added a motivation and link to the ari format

2026-03-11T09:04:19Z

Added a motivation and link to the ari format

JCKassing: JCKassing moved page Category TRS Standard to TRS Standard: removed Category

2026-03-09T09:29:55Z

JCKassing moved page Category TRS Standard to TRS Standard: removed Category

JCKassing: Added TRS Standard Category Page

2026-03-09T09:28:57Z

Added TRS Standard Category Page

New page

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 [[Term Rewriting | here]].

Formally, a term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules, see [1].

A term rewrite system R is terminating if there exists no infinite rewrite sequence s0 →R s1 →R s1 →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.

[[Category:Categories]]

@@ Line 1: / Line 1: @@
 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 [[Term Rewriting | here]].
+The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]] and [https://project-coco.uibk.ac.at/ARI/trs.php here].
 Formally, a term rewrite system R = {l<sub>1</sub> &rarr; r<sub>1</sub>,...,l<sub>n</sub> &rarr; r<sub>n</sub>} is a finite set of rewrite rules, see [1].

← Older revision	Revision as of 09:29, 9 March 2026
(No difference)