Termination-Portal.org - User contributions [en]

Suggestions

2026-03-19T10:44:34Z

JCKassing: Updated suggestions

Suggestions to improve this web site 

TODO:

* create/fill the pages on the different categories used in the termination competition (listed here: http://www.termination-portal.org/wiki/Termination_Competition).

Termination Competition

2026-03-19T10:38:03Z

JCKassing: Added TRS Complexity pages

TRS Parallel Innermost Derivational Complexity

2026-03-19T10:36:30Z

JCKassing: Added TRS Parallel Innermost Derivational Complexity

The TRS Innermost Derivational Complexity category is concerned with the question "What is the time complexity of algorithms represented by a given TRS with relation to the size of the initial term if we only consider innermost rewriting".

== Category Motivation ==

Analyzing the time complexity of a rewrite system is interesting because it reveals how its performance scales as input size grows.

Moreover, since innermost rewriting (call-by-value) is one of the most important evaluation strategies,
it is an interesting restriction to find bounds on the innermost time complexity.

== Syntax & Semantic ==

TODO: clarify the difference to [TRS Innermost Derivational Complexity | TRS Innermost Derivational Complexity]!

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 = {l1 → r1,...,ln → rn} is a finite set of rewrite rules.

Let |t| be the size of the term t, i.e., the number of its positions.
Then the innermost derivation height dh(t) of a term t is the supremum over all →iR-rewrite sequences starting with t.

We split the function symbols into defined symbols (those that occur at the root of a left-hand side of a rule, the algorithms)
and constructor symbols (the remaining function symbols, the data).
A basic term t has a defined symbol at the root and otherwise only constructors and variables, i.e., it represents an algorithm that is given fixed input data.
The set of all basic terms is denoted TB.

The innermost derivational complexity of an ARS is a function that maps every natural number n
to the greatest derivation height of all basic terms of size at most n, i.e., dc→R (n) = sup{m | t ∈ TB, |t| <= n, t →iRn s}.

The goal is to find an asymptotic upper bound and lower bound on the innermost derivational complexity of a given TRS R.
Possible complexity classes are O(1), O(n), O(n2), ..., O(EXP), O(2-EXP).
The '?' indicates that no bound was found.

== Problem ==

Input: A term rewrite system R.

Question: What is the asymptotic innermost derivational complexity of R?

Possible Outputs:
* "WORST_CASE(f(n),g(n))" where f(n) and g(n) are lower and upper complexity bounds, respectively, or '?', followed by a proof of these bounds, e.g., a ranking function proving termination of R.
* "MAYBE" (indicating that the solver cannot prove any complexity bound).

== References ==

[[Category:Categories]]

TRS Innermost Runtime Complexity

2026-03-19T10:34:45Z

JCKassing: Added TRS Innermost Runtime Complexity

The TRS Innermost Runtime Complexity category is concerned with the question "What is the time complexity of algorithms represented by a given TRS with relation to the size of the initial term if we only consider innermost rewriting".

== Category Motivation ==

Analyzing the time complexity of a rewrite system is interesting because it reveals how its performance scales as input size grows.

While derivational complexity considers arbitrary initial terms, runtime complexity restricts the initial terms to model an algorithm that is given fixed data as arguments,
which relates to the intuitive definition of time complexity.

Moreover, since innermost rewriting (call-by-value) is one of the most important evaluation strategies,
it is an interesting restriction to find bounds on the innermost time complexity.

== Syntax & Semantic ==

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 = {l1 → r1,...,ln → rn} is a finite set of rewrite rules.

Let |t| be the size of the term t, i.e., the number of its positions.
Then the innermost derivation height dh(t) of a term t is the supremum over all →iR-rewrite sequences starting with t.

We split the function symbols into defined symbols (those that occur at the root of a left-hand side of a rule, the algorithms)
and constructor symbols (the remaining function symbols, the data).
A basic term t has a defined symbol at the root and otherwise only constructors and variables, i.e., it represents an algorithm that is given fixed input data.
The set of all basic terms is denoted TB.

The innermost runtime complexity of an ARS is a function that maps every natural number n
to the greatest derivation height of all basic terms of size at most n, i.e., dc→R (n) = sup{m | t ∈ TB, |t| <= n, t →iRn s}.

The goal is to find an asymptotic upper bound and lower bound on the innermost runtime complexity of a given TRS R.
Possible complexity classes are O(1), O(n), O(n2), ..., O(EXP), O(2-EXP).
The '?' indicates that no bound was found.

== Problem ==

Input: A term rewrite system R.

Question: What is the asymptotic innermost runtime complexity of R?

Possible Outputs:
* "WORST_CASE(f(n),g(n))" where f(n) and g(n) are lower and upper complexity bounds, respectively, or '?', followed by a proof of these bounds, e.g., a ranking function proving termination of R.
* "MAYBE" (indicating that the solver cannot prove any complexity bound).

== References ==

[[Category:Categories]]

TRS Runtime Complexity

2026-03-19T10:33:01Z

JCKassing: Added TRS Runtime Complexity

The TRS Runtime Complexity category is concerned with the question "What is the time complexity of algorithms represented by a given TRS with relation to the size of the initial term".

== Category Motivation ==

Analyzing the time complexity of a rewrite system is interesting because it reveals how its performance scales as input size grows.

While derivational complexity considers arbitrary initial terms, runtime complexity restricts the initial terms to model an algorithm that is given fixed data as arguments,
which relates to the intuitive definition of time complexity.

== Syntax & Semantic ==

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 = {l1 → r1,...,ln → rn} is a finite set of rewrite rules.

Let |t| be the size of the term t, i.e., the number of its positions.
Then the derivation height dh(t) of a term t is the supremum over all →R-rewrite sequences starting with t.

We split the function symbols into defined symbols (those that occur at the root of a left-hand side of a rule, the algorithms)
and constructor symbols (the remaining function symbols, the data).
A basic term t has a defined symbol at the root and otherwise only constructors and variables, i.e., it represents an algorithm that is given fixed input data.
The set of all basic terms is denoted TB.

The runtime complexity of an ARS is a function that maps every natural number n
to the greatest derivation height of all basic terms of size at most n, i.e., dc→R (n) = sup{m | t ∈ TB, |t| <= n, t →Rn s}.

The goal is to find an asymptotic upper bound and lower bound on the runtime complexity of a given TRS R.
Possible complexity classes are O(1), O(n), O(n2), ..., O(EXP), O(2-EXP).
The '?' indicates that no bound was found.

== Problem ==

Input: A term rewrite system R.

Question: What is the asymptotic runtime complexity of R?

Possible Outputs:
* "WORST_CASE(f(n),g(n))" where f(n) and g(n) are lower and upper complexity bounds, respectively, or '?', followed by a proof of these bounds, e.g., a ranking function proving termination of R.
* "MAYBE" (indicating that the solver cannot prove any complexity bound).

== References ==

[[Category:Categories]]

TRS Innermost Derivational Complexity

2026-03-19T10:26:59Z

JCKassing: Added TRS Innermost Derivational Complexity

The TRS Innermost Derivational Complexity category is concerned with the question "What is the time complexity of a given TRS with relation to the size of the initial term if we only consider innermost rewriting".

== Category Motivation ==

Analyzing the time complexity of a rewrite system is interesting because it reveals how its performance scales as input size grows.
his helps to detect rewrite systems that seem fine for small inputs but become impractical for large problems.

Moreover, since innermost rewriting (call-by-value) is one of the most important evaluation strategies,
it is an interesting restriction to find bounds on the innermost time complexity.

== Syntax & Semantic ==

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 = {l1 → r1,...,ln → rn} is a finite set of rewrite rules.

Let |t| be the size of the term t, i.e., the number of its positions.
Then the innermost derivation height dh(t) of a term t is the supremum over all innermost →iR-rewrite sequences starting with t.
The innermost derivational complexity of an ARS is a function that maps every natural number n
to the greatest derivation height of all objects of size at most n, i.e., dc→R (n) = sup{m | |t| <= n, t →iRn s}.

The goal is to find an asymptotic upper bound and lower bound on the derivational complexity of a given TRS R.
Possible complexity classes are O(1), O(n), O(n^2), O(n^3), ..., O(EXP), O(2-EXP).
The '?' indicates that no bound was found.

== Problem ==

Input: A term rewrite system R.

Question: What is the asymptotic innermost derivational complexity of R?

Possible Outputs:
* "WORST_CASE(f(n),g(n))" where f(n) and g(n) are lower and upper complexity bounds, respectively, or '?', followed by a proof of these bounds, e.g., a ranking function proving termination of R.
* "MAYBE" (indicating that the solver cannot prove any complexity bound).

== References ==

[[Category:Categories]]

TRS Derivational Complexity

2026-03-19T10:23:56Z

JCKassing: Added TRS Derivational Complexity

The TRS Derivational Complexity category is concerned with the question "What is the time complexity of a given TRS with relation to the size of the initial term".

== Category Motivation ==

Analyzing the time complexity of a rewrite system is interesting because it reveals how its performance scales as input size grows.
his helps to detect rewrite systems that seem fine for small inputs but become impractical for large problems.

== Syntax & Semantic ==

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 = {l1 → r1,...,ln → rn} is a finite set of rewrite rules.

Let |t| be the size of the term t, i.e., the number of its positions.
Then the derivation height dh(t) of a term t is the supremum over all →R-rewrite sequences starting with t.
The derivational complexity of an ARS is a function that maps every natural number n
to the greatest derivation height of all objects of size at most n, i.e., dc→R (n) = sup{m | |t| <= n, t →Rn s}.

The goal is to find an asymptotic upper bound and lower bound on the derivational complexity of a given TRS R.
Possible complexity classes are O(1), O(n), O(n2), ..., O(EXP), O(2-EXP).
The '?' indicates that no bound was found.

== Problem ==

Input: A term rewrite system R.

Question: What is the asymptotic derivational complexity of R?

Possible Outputs:
* "WORST_CASE(f(n),g(n))" where f(n) and g(n) are lower and upper complexity bounds, respectively, or '?', followed by a proof of these bounds, e.g., a ranking function proving termination of R.
* "MAYBE" (indicating that the solver cannot prove any complexity bound).

== References ==

[[Category:Categories]]

String Rewriting

2026-03-18T11:46:09Z

JCKassing: Blanked the page

Transition Systems

2026-03-18T11:43:18Z

JCKassing: No Category anymore

Syntax and semantics of the format are presented in [https://www.microsoft.com/en-us/research/publication/termcomp-proposal-pushdown-systems-as-a-model-for-programs-with-procedures/].

Termination Competition

2026-03-18T11:41:02Z

JCKassing: Added all termination category subpages

Integer Transition Systems

2026-03-18T11:40:28Z

JCKassing: Added ITS Page

The Integer Transition Systems category is concerned with the question "Will every possible sequence of rewrite steps on an integer program terminate?".

== Syntax & Semantic ==

Integer Transition Systems (ITSs) are [https://project-coco.uibk.ac.at/ARI/lctrs.php LCTRSs] with the following restrictions:
* The theory is always Ints.
* Rules must comply with the following grammar:
<pre>
rule ::= (rule lhs rhs (:guard term)? (:var (vars))?)
lhs ::= (identifier identifier+)
rhs ::= (identifier term+)
</pre>
Moreover, ITSs must declare one and only one entrypoint
<pre>
entrypoint ::= (entrypoint identifier)
</pre>
where the given identifier refers to a previously declared function symbol.

The goal is to prove termination w.r.t. all well-sorted startterms of the form
<pre>
(f c_1 ... c_k)
</pre>
where f is the entrypoint and c_1,...,c_k are constants from the theory Ints (i.e., integers or Booleans).

== Problem ==

Input: An ITS 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 of R.
* "MAYBE" (indicating that the solver cannot prove termination of R).

== References ==

[[Category:Categories]]

TRS Conditional

2026-03-18T11:37:59Z

JCKassing: Added TRS Conditional Page

The TRS Conditional category is concerned with the question "Will every possible sequence of conditional rewrites steps terminate?"
where a conditional rewrite step may depend on the reachability between two independent terms, e.g., can 'leq(t,s)' be evaluated to 'true'?

== Syntax & Semantic ==

Formally, a conditional term rewrite system is a set R = {l1 → r1 | c1,...,ln → rn | cn} of finitely many conditional rewrite rules.
A conditional rewrite rule is a rewrite rule l → r with an additional condition, a reachability constraint, that has to be satisfied to use the rewrite rule.
There are multiple different ways one can interpret these conditions, e.g., oriented, joined, and convertible.

== Problem ==

Input: A conditional 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 of R.
* "MAYBE" (indicating that the solver cannot prove termination of R).

== References ==

[[Category:Categories]]

TRS Conditional - Operational Termination

2026-03-18T11:37:52Z

JCKassing: Added TRS Conditional - Operation Page

The TRS Conditional category is concerned with the question "Will every possible sequence of conditional rewrites steps terminate?"
where a conditional rewrite step may depend on the reachability between two independent terms, e.g., can 'leq(t,s)' be evaluated to 'true'?

== Syntax & Semantic ==

Formally, a conditional term rewrite system is a set R = {l1 → r1 | c1,...,ln → rn | cn} of finitely many conditional rewrite rules.
A conditional rewrite rule is a rewrite rule l → r with an additional condition, a reachability constraint, that has to be satisfied to use the rewrite rule.
There are multiple different ways one can interpret these conditions, e.g., oriented, joined, and convertible.

TODO: clarify the difference to [[TRS Conditional|TRS Conditional]]!

== Problem ==

Input: A conditional 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 of R.
* "MAYBE" (indicating that the solver cannot prove termination of R).

== References ==

[[Category:Categories]]

TRS Equational

2026-03-18T11:29:46Z

JCKassing: Added TRS Equational Page

The TRS Equational category is concerned with the question "Will every possible sequence of rewrites steps on equivalence classes terminate?".

== Syntax & Semantic ==

Formally, an equational term rewrite system is a set R = {l1 → r1,...,ln → rn} of finitely rewrite rules together a set S = {a1 = b1,...,an = bn} of finitely many term equations, called a ''theory''.

An equational term rewrite system R/S is terminating if there exists no infinite rewrite sequence s00 →R s01 =S ... =S s10 →R s11 =S ... =S s20 →R ..., i.e., no infinite rewrite sequence that uses infinitely many rules from R where we can use the equations from S mid rewriting.

Here, a ''theory'' may be added to declarations of function symbols.

<pre>
fun ::= ( fun identifier number theory? )
theory ::= :theory [A | C | AC]
</pre>

* full rewriting modulo associativity / commutativity / associativity and commutativity

== Problem ==

Input: n equational term rewrite system R/S.

Question: Does R/S terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R/S.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence that uses infinitely many rules from R.
* "MAYBE" (indicating that the solver cannot prove termination of R/S).

== References ==

[[Category:Categories]]

TRS Contextsensitive

2026-03-18T11:25:18Z

JCKassing: Added TRS Contextsensitive Page

The TRS Contextsensitive category is concerned with the question "Will every possible sequence of rewrites eventually stop if we prohibit to rewrite within certain arguments of function symbols".

== Category Motivation ==

Context-sensitive rewriting is a restriction of first-order term rewriting which is used, e.g., to model different evaluation strategies for the analysis of functional programming languages.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Term Rewriting | here]] and specifically for context-sensitive rewriting [https://project-coco.uibk.ac.at/ARI/cstrs.php here].

Formally, a term rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules, see [1].
Additionally, every n-ary function symbbol f has a corresponding replacement map μ(f) which indicates which arguments of f may be evaluated.

A term rewrite system R is terminating w.r.t. μ if there exists no infinite rewrite sequence s0 →R s1 →R s1 →R ... that respects the replacement map μ.

== Problem ==

Input: A term rewrite system R and a replacement map μ

Question: Does R terminate w.r.t. μ?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R w.r.t. μ.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence w.r.t. μ.
* "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]]

PTRS Standard

2026-03-11T10:08:02Z

JCKassing: Added missing reference

The PTRS Standard category is concerned with the question "Will every rewrite sequence eventually stop with probability 1 (almost-sure termination) and does every start term t has a finite upper bound on the expected runtime of all rewrite sequences starting with t (strong almost sure-termination)?".

The category was first used in the termination competition in 2024, after an initial in-person event for probabilistic termination provers at the [[19th_International_Workshop_on_Termination | termination workshop 2023]].

== Category Motivation ==

This category investigates different notions of termination of probabilistic term rewrite systems, where rewrite rules are applied according to probability distributions.

Many algorithms can be made more robust by introducing probabilistic choices.
For example, in probabilistic quicksort the pivot element is chosen uniformly at random.
This variant is more robust than the standard quicksort algorithm because it achieves an expected runtime of O(n * log(⁡n))
for every input and avoids the deterministic worst-case runtime of O(n2).
However, when probabilities are introduced, programmers often quickly lose intuition about expected runtime and termination.
Therefore, automatic techniques for proving termination and establishing upper bounds on the expected runtime are needed.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Probabilistic_Rewriting | here]] including the definitions of almost-sure termination (AST) and strong almost-sure termination (SAST).
Note that the third notion of termination 'positive almost-sure termination' (PAST) is currently not supported by any Tool.
However, in [2] it was shown that PAST and SAST are almost the same for probabilistic rewriting, hence it suffices to analyze the stronger notion SAST.
In fact, PAST and SAST are equivalent for finite PTRSs that contain at least a single function symbol of arity at least 2 (that has more than 2 arguments).

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

== Problem ==

Input: A probabilistic term rewrite system R.

Question: Is R AST or SAST?

Possible Outputs:
* "AST" followed by a termination proof, e.g., a ranking function proving almost-sure termination (AST) of R.
* "SAST" followed by a termination proof, e.g., a ranking function proving strong almost-sure termination (SAST) of R.
* "MAYBE" (indicating that the solver can neither prove AST nor SAST termination).

== References ==

* [1] Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. Science of Computer Programming, 2020.
* [2] Jan-Christoph Kassing and Jürgen Giesl. From Innermost To Full Probabilistic Term Rewriting: Almost-Sure Termination, Complexity, And Modularity. Logical Methods in Computer Science, 2026.

[[Category:Categories]]

PTRS Innermost

2026-03-11T10:07:37Z

JCKassing: Fixed small typo in reference

The PTRS Standard category is concerned with the question "Will every innermost rewrite sequence eventually stop with probability 1 (almost-sure termination) and does every start term t has a finite upper bound on the expected runtime of all innermost rewrite sequences starting with t (strong almost sure-termination)?".

The category was first used in the termination competition in 2024, after an initial in-person event for probabilistic termination provers at the [[19th_International_Workshop_on_Termination | termination workshop 2023]].

== Category Motivation ==

This category investigates different notions of termination of probabilistic term rewrite systems, where rewrite rules are applied according to probability distributions.
It restricts the analysis of probabilistic algorithms to a call-by-value evaluation strategy, which is one of the most used evaluation strategies in probabilistic programming languages.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Probabilistic_Rewriting | here]] including the definitions of almost-sure termination (AST) and strong almost-sure termination (SAST).
Note that the third notion of termination 'positive almost-sure termination' (PAST) is currently not supported by any Tool.
However, in [2] it was shown that PAST and SAST are almost the same for probabilistic rewriting, hence it suffices to analyze the stronger notion SAST.
In fact, PAST and SAST are equivalent for finite PTRSs that contain at least a single function symbol of arity at least 2 (that has more than 2 arguments).

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

An innermost rewrite step is a rewrite step that rewrites an innermost reducible expression, i.e., no proper subterm is reducible using the rules from R.

== Problem ==

Input: A probabilistic term rewrite system R.

Question: Is R innermost AST or innermost SAST?

Possible Outputs:
* "iAST" followed by a termination proof, e.g., a ranking function proving innermost almost-sure termination (iAST) of R.
* "iSAST" followed by a termination proof, e.g., a ranking function proving innermost strong almost-sure termination (iSAST) of R.
* "MAYBE" (indicating that the solver can neither prove iAST nor iSAST termination).

== References ==

* [1] Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. Science of Computer Programming, 2020.
* [2] Jan-Christoph Kassing and Jürgen Giesl. From Innermost To Full Probabilistic Term Rewriting: Almost-Sure Termination, Complexity, And Modularity. Logical Methods in Computer Science, 2026.

[[Category:Categories]]

Probabilistic Rewriting

2026-03-11T10:05:58Z

JCKassing: Removed Categories from this page

== General ==

As in the non-probabilistic setting, we use an adaption of the [https://project-coco.uibk.ac.at/ARI/ ARI format], so probabilistic TRSs (PTRSs) are represented as S-Expressions (see [https://smt-lib.org/papers/smt-lib-reference-v2.6-r2021-05-12.pdf here, Sec. 3.1]). The format of TRSs is explained [[Term Rewriting|here]]. To extend this format for PTRSs, rules are replaced by probabilistic rules that are defined as follows:
<pre>
prule ::= ( prule term dist cost? )
cost ::= :cost number
dist ::= ( ( term prob? )* )
prob ::= :prob number
</pre>

Some examples of valid PTRSs are shown below.

<pre>
===== P1 =====
(format PTRS)
(fun f 0)
(fun stop 0)
(prule f (( f :prob 1 ) (stop :prob 1 )))
</pre>
* P1 models a coin flip that stops once it flips heads and keeps on going if it flips tails.
<pre>
===== P2 =====
(format PTRS)
(fun g 1)
(prule (g x) (( (g (g x)) :prob 1 ) (x :prob 1 )))
</pre>
* P2 models a symmetric random walk on the numbers of f symbols in a term.
<pre>
===== P3 =====
(format PTRS)
(fun h 1)
(prule (h x) (( (h (h x)) :prob 2 ) (x :prob 1 )))
</pre>
* P3 models a biased random walk on the numbers of h symbols in a term which is biased towards nontermination.

== Probabilistic Termination ==

There are several notions of ``termination'' in the probabilistic setting.
As in ordinary term rewriting, we consider universal termination, i.e., we have no fixed start term, but consider every possible reduction.
For the formal definitions of all notions of termination, see [https://www.sciencedirect.com/science/article/pii/S0167642319301339 here].

===== Certain Termination =====

A PTRS is certainly terminating if every possible reduction eventuelly terminates.
As this boils down to termination of TRSs, we usually try to omit certainly terminating examples in the following category,
and hence, have no allowed answer for a certainly terminating PTRS.

Example: None of the PTRSs P1, P2, or P3 are certainly terminating.

===== Almost-Sure Termination (AST) =====

A PTRS is almost-surely terminating if every non-terminating reduction occurs with probability 0.

Example: While P1 and P2 are AST, P3 is not AST.

===== Positive Almost-Sure Termination (PAST) =====

A PTRS is positive almost-surely terminating if the expected derivation length of every possible reduction is finite.

Example: Only P1 is PAST, but P2 and P3 are not PAST.

===== Strong Almost-Sure Termination (SAST) =====

A PTRS is strong almost-surely terminating if for every start term t there exists a bound C_t such that
the expected derivation length of every possible reduction starting in t is at most C_t.

Example: Again only P1 is PAST, but P2 and P3 are not PAST.

Termination Competition

2026-03-11T10:03:58Z

JCKassing: Added links to some defined categories

PTRS Innermost

2026-03-11T10:03:05Z

JCKassing: Added PTRS Innermost category

The PTRS Standard category is concerned with the question "Will every innermost rewrite sequence eventually stop with probability 1 (almost-sure termination) and does every start term t has a finite upper bound on the expected runtime of all innermost rewrite sequences starting with t (strong almost sure-termination)?".

The category was first used in the termination competition in 2024, after an initial in-person event for probabilistic termination provers at the [[19th_International_Workshop_on_Termination | termination workshop 2023]].

== Category Motivation ==

This category investigates different notions of termination of probabilistic term rewrite systems, where rewrite rules are applied according to probability distributions.
It restricts the analysis of probabilistic algorithms to a call-by-value evaluation strategy, which is one of the most used evaluation strategies in probabilistic programming languages.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Probabilistic_Rewriting | here]] including the definitions of almost-sure termination (AST) and strong almost-sure termination (SAST).
Note that the third notion of termination 'positive almost-sure termination' (PAST) is currently not supported by any Tool.
However, in [2] it was shown that PAST and SAST are almost the same for probabilistic rewriting, hence it suffices to analyze the stronger notion SAST.
In fact, PAST and SAST are equivalent for finite PTRSs that contain at least a single function symbol of arity at least 2 (that has more than 2 arguments).

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

An innermost rewrite step is a rewrite step that rewrites an innermost reducible expression, i.e., no proper subterm is reducible using the rules from R.

== Problem ==

Input: A probabilistic term rewrite system R.

Question: Is R innermost AST or innermost SAST?

Possible Outputs:
* "iAST" followed by a termination proof, e.g., a ranking function proving innermost almost-sure termination (iAST) of R.
* "iSAST" followed by a termination proof, e.g., a ranking function proving innermost strong almost-sure termination (iSAST) of R.
* "MAYBE" (indicating that the solver can neither prove iAST nor iSAST termination).

== References ==

* [1] Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. Science of Computer Programming, 2020.
* [1] Jan-Christoph Kassing and Jürgen Giesl. From Innermost To Full Probabilistic Term Rewriting: Almost-Sure Termination, Complexity, And Modularity. Logical Methods in Computer Science, 2026.

[[Category:Categories]]

PTRS Standard

2026-03-11T09:57:07Z

JCKassing: Added PTRS Standard category

The PTRS Standard category is concerned with the question "Will every rewrite sequence eventually stop with probability 1 (almost-sure termination) and does every start term t has a finite upper bound on the expected runtime of all rewrite sequences starting with t (strong almost sure-termination)?".

The category was first used in the termination competition in 2024, after an initial in-person event for probabilistic termination provers at the [[19th_International_Workshop_on_Termination | termination workshop 2023]].

== Category Motivation ==

This category investigates different notions of termination of probabilistic term rewrite systems, where rewrite rules are applied according to probability distributions.

Many algorithms can be made more robust by introducing probabilistic choices.
For example, in probabilistic quicksort the pivot element is chosen uniformly at random.
This variant is more robust than the standard quicksort algorithm because it achieves an expected runtime of O(n * log(⁡n))
for every input and avoids the deterministic worst-case runtime of O(n2).
However, when probabilities are introduced, programmers often quickly lose intuition about expected runtime and termination.
Therefore, automatic techniques for proving termination and establishing upper bounds on the expected runtime are needed.

== Syntax & Semantic ==

The syntax and the semantics of term rewrite systems are described [[Probabilistic_Rewriting | here]] including the definitions of almost-sure termination (AST) and strong almost-sure termination (SAST).
Note that the third notion of termination 'positive almost-sure termination' (PAST) is currently not supported by any Tool.
However, in [2] it was shown that PAST and SAST are almost the same for probabilistic rewriting, hence it suffices to analyze the stronger notion SAST.
In fact, PAST and SAST are equivalent for finite PTRSs that contain at least a single function symbol of arity at least 2 (that has more than 2 arguments).

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

== Problem ==

Input: A probabilistic term rewrite system R.

Question: Is R AST or SAST?

Possible Outputs:
* "AST" followed by a termination proof, e.g., a ranking function proving outermost termination of R.
* "SAST" followed by a termination proof, e.g., a ranking function proving outermost termination of R.
* "MAYBE" (indicating that the solver cannot prove outermost termination).

== References ==

* [1] Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. Science of Computer Programming, 2020.

[[Category:Categories]]

TRS Outermost

2026-03-11T09:11:45Z

JCKassing: Added a motivation and link to the ari format (TRS Outermost)

The TRS Outermost category is concerned with the question "Will every outermost rewrite sequence eventually stop?".
In other words, does every computation defined by the rewrite rules that only evaluates outermost reducible expressions eventually reach a normal form (a term where no rule applies)?

== Category Motivation ==

This category investigates termination under the outermost rewriting strategy, roughly corresponding to a call-by-name or lazy evaluation strategy.
Although it is not the most common evaluation strategy in programming languages, it is still used by some widely used languages, such as Haskell.

== Syntax & Semantic ==

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 = {l1 → r1,...,ln → rn} is a finite set of rewrite rules, see [1].

An outermost rewrite step is a rewrite step that rewrites an outermost reducible expression, i.e., there is no other redex at a position above the redex we want to rewrite.
A term rewrite system R is outermost terminating if there exists no infinite rewrite sequence s0 →oR s1 →oR s2 →oR ...

== Problem ==

Input: A term rewrite system R.

Question: Does R outermost terminate?

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

== References ==

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

[[Category:Categories]]

TRS Innermost

2026-03-11T09:08:30Z

JCKassing: Added a motivation and link to the ari format (TRS Innermost)

The TRS Innermost category is concerned with the question "Will every innermost rewrite sequence eventually stop?".
In other words, does every computation defined by the rewrite rules that only evaluates innermost reducible expressions eventually reach a normal form (a term where no rule applies)?

== Category Motivation ==

This category investigates termination under the innermost rewriting strategy, roughly corresponding to a call-by-value evaluation strategy in programming languages,
which is one of the most used evaluation strategies.

== Syntax & Semantic ==

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 = {l1 → r1,...,ln → rn} is a finite set of rewrite rules, see [1].

An innermost rewrite step is a rewrite step that rewrites an innermost reducible expression, i.e., no proper subterm is reducible using the rules from R.
A term rewrite system R is innermost terminating if there exists no infinite rewrite sequence s0 →iR s1 →iR s2 →iR ...

== Problem ==

Input: A term rewrite system R.

Question: Does R innermost terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving innermost termination of R.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite innermost 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]]

TRS Standard

2026-03-11T09:04:19Z

JCKassing: Added a motivation and link to the ari format

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)?

== Category Motivation ==

This category evaluates tools on termination of standard first-order term rewrite systems with unrestricted rewriting which is one of the basic problems in the competition. Many of the other termination problems are either special forms of this problem, or can be reduced to this problem.

== Syntax & Semantic ==

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 = {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]]

SRS Standard

2026-03-10T16:27:46Z

JCKassing: Mentioned strings in the def of SRSs

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 [[Term Rewriting | here]].
Strings are terms where every function symbol has arity 1, i.e., exactly one argument.

Formally, a string rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules where all occurring terms are strings.

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

[[Category:Categories]]

SRS Relative

2026-03-10T16:27:05Z

JCKassing: Added SRS Relative Category Page

The SRS Relative category is concerned with the question "Will every possible sequence of rewrite steps on strings eventually stop using a certain subset of the given rewrite rules?".
In other words, if every rule has a cost which is either 0 or 1, then does every possible reduction has a finite total cost?

== Syntax & Semantic ==

Strings are terms where every function symbol has arity 1, i.e., exactly one argument.
Formally, a relative string rewrite system is a set R = {l1 → r1,...,ln → rn} and a set S = {a1 → b1,...,an → bn} of finitely many rewrite rules denoted by R/S where all the occuring terms are strings.

A relative string rewrite system R/S is terminating if there exists no infinite rewrite sequence s00 →R s01 →S ... →S s10 →R s11 →S ... →S s20 →R ..., i.e., no infinite rewrite sequence that uses infinitely many rules from R.

Instead of the two seperate sets, one typically gives costs of 0 or 1 to every rule.
Rules with cost 1 are in R and rules with costs 0 are in S.
Then, relative termination is equal to the statement that every possible reduction has a finite total cost.
The syntax and the semantics of string rewrite systems with costs at the rules are described [[Term Rewriting | here]].

== Problem ==

Input: A relative string rewrite system R/S.

Question: Does R/S terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R/S.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence that uses infinitely many rules from R.
* "MAYBE" (indicating that the solver cannot prove termination of R/S).

[[Category:Categories]]

SRS Standard

2026-03-10T16:24:41Z

JCKassing: Added SRS Standard Category Page

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 [[Term Rewriting | here]].
Strings are terms where every function symbol has arity 1, i.e., exactly one argument.

Formally, a string rewrite system R = {l1 → r1,...,ln → rn} is a finite set of rewrite rules.

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

[[Category:Categories]]

TRS Relative

2026-03-09T17:12:38Z

JCKassing: Fixed some typos

The TRS Relative category is concerned with the question "Will every possible sequence of rewrites eventually stop using a certain subset of the given rewrite rules?".
In other words, ifevery rule has a cost which is either 0 or 1, then does every possible reduction has a finite total cost?

== Syntax & Semantic ==

Formally, a relative term rewrite system is a set R = {l1 → r1,...,ln → rn} and a set S = {a1 → b1,...,an → bn} of finitely many rewrite rules denoted by R/S, see [1].

A relative term rewrite system R/S is terminating if there exists no infinite rewrite sequence s00 →R s01 →S ... →S s10 →R s11 →S ... →S s20 →R ..., i.e., no infinite rewrite sequence that uses infinitely many rules from R.

Instead of the two seperate sets, one typically gives costs of 0 or 1 to every rule.
Rules with cost 1 are in R and rules with costs 0 are in S.
Then, relative termination is equal to the statement that every possible reduction has a finite total cost.
The syntax and the semantics of term rewrite systems with costs at the rules are described [[Term Rewriting | here]].

== Problem ==

Input: A relative term rewrite system R/S.

Question: Does R/S terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R/S.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence that uses infinitely many rules from R.
* "MAYBE" (indicating that the solver cannot prove termination of R/S).

== References ==

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

[[Category:Categories]]

TRS Outermost

2026-03-09T17:11:44Z

JCKassing: Added TRS Outermost Category Page

The TRS Outermost category is concerned with the question "Will every outermost rewrite sequence eventually stop?".
In other words, does every computation defined by the rewrite rules that only evaluates outermost reducible expressions 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].

An outermost rewrite step is a rewrite step that rewrites an outermost reducible expression, i.e., there is no other redex at a position above the redex we want to rewrite.
A term rewrite system R is outermost terminating if there exists no infinite rewrite sequence s0 →oR s1 →oR s2 →oR ...

== Problem ==

Input: A term rewrite system R.

Question: Does R outermost terminate?

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

== References ==

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

[[Category:Categories]]

TRS Innermost

2026-03-09T17:09:10Z

JCKassing: Added TRS Innermost Category Page

The TRS Innermost category is concerned with the question "Will every innermost rewrite sequence eventually stop?".
In other words, does every computation defined by the rewrite rules that only evaluates innermost reducible expressions 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].

An innermost rewrite step is a rewrite step that rewrites an innermost reducible expression, i.e., no proper subterm is reducible using the rules from R.
A term rewrite system R is innermost terminating if there exists no infinite rewrite sequence s0 →iR s1 →iR s2 →iR ...

== Problem ==

Input: A term rewrite system R.

Question: Does R innermost terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving innermost termination of R.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite innermost 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]]

TRS Relative

2026-03-09T09:48:02Z

JCKassing: Added TRS Relative Category Page

The TRS Relative category is concerned with the question "Will every possible sequence of rewrites eventually stop using a certain subset of the given rewrite rules?".
In other words, ifevery rule has a cost which is either 0 or 1, then does every possible reduction has a finite total cost?

== Syntax & Semantic ==

Formally, a relative term rewrite system is a set R = {l1 → r1,...,ln → rn} and a set S = {a1 → b1,...,an → bn} of finitely many rewrite rules denoted by R/S, see [1].

A relative term rewrite system R is terminating if there exists no infinite rewrite sequence s00 →R s01 →S ... →S s10 →R s11 →S ... →S s20 →R ..., i.e., no infinite rewrite sequence that uses infinitely many rules from R.

Instead of the two seperate sets, one typically gives costs of 0 or 1 to every rule.
Rules with cost 1 are in R and rules with costs 0 are in S.
Then, relative termination is equal to the statement that every possible reduction has a finite total cost.
The syntax and the semantics of term rewrite systems with costs at the rules are described [[Term Rewriting | here]].

== Problem ==

Input: A relative term rewrite system R/S.

Question: Does R terminate?

Possible Outputs:
* "YES" followed by a termination proof, e.g., a ranking function proving termination of R/S.
* "NO" followed by a nontermination proof, e.g., a loop that indicates an infinite rewrite sequence that uses infinitely many rules from R.
* "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]]

Termination Competition

2026-03-09T09:31:03Z

JCKassing: Added Link to new TRS Standard category page

TRS Standard

2026-03-09T09:29:55Z

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

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]]

Category TRS Standard

2026-03-09T09:29:55Z

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

#REDIRECT [[TRS Standard]]

TRS Standard

2026-03-09T09:28:57Z

JCKassing: Added TRS Standard Category 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]]

Termination Competition History

2026-03-08T12:40:18Z

JCKassing: Added results

The following competitions have taken place:

* [[Termination Competition 2025]] affiliated with [https://www.imn.htwk-leipzig.de/WST2025/ WST 2025], [https://termcomp.github.io/Y2025/ Results].
* [[Termination Competition 2024]] affiliated with [https://merz.gitlabpages.inria.fr/2024-ijcar/ IJCAR 2024], [https://termcomp.github.io/Y2024/ Results].
* [[Termination Competition 2023]] affiliated with [[WST2023]], [https://termcomp.github.io/Y2023/ Results].
* [[Termination Competition 2022]] affiliated with [https://easychair.org/smart-program/FLoC2022/IJCAR-index.html IJCAR 2022], [https://termcomp.github.io/Y2022/ Results].
* [[Termination Competition 2021]] affiliated with [http://www.cs.cmu.edu/~mheule/CADE28/ CADE 2021], [https://termcomp.github.io/Y2021/ Results].
* [[Termination Competition 2020]] affiliated with [https://ijcar2020.org/ IJCAR 2020], [https://termcomp.github.io/Y2020/ Results].
* [[Termination Competition 2019]] affiliated with [https://tacas.info/toolympics.php Toolympics at TACAS 2019], [https://termcomp.github.io/Y2019/ Results].
* [[Termination Competition 2018]] affiliated with FLoC 2018, Oxford, UK, July 13, 2018, [https://termcomp.github.io/Y2018/ Results].

* [[Termination_Competition_2017|Termination Competition 2017]] affiliated with [http://www.cs.ox.ac.uk/conferences/fscd2017/ FSCD], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2017 Results of Competition], [http://termcomp.imn.htwk-leipzig.de/competitions/67 Results of demonstration].

* [[Termination_Competition_2016|Termination Competition 2016]] affiliated with [http://cl-informatik.uibk.ac.at/events/wst-2016/ WST (Workshop on Termination)], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2016 Results of Competition]. [http://www.cs.upc.edu/~albert/papers/termcomp2016_slides.pdf Presentation at WST]

* [[Termination Competition 2015]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2015 Results of Competition], [http://www.cs.upc.edu/~albert/papers/termCompCADE2015.pdf Description paper at CADE-25] [http://www.cs.upc.edu/~albert/papers/termcomp2015_slides.pdf Report]

* [[Termination Competition 2014]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2014 Results of Competition], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/23 Results of Demonstration]

* [[Termination Competition 2013]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=437763 Results], [http://termcomp.uibk.ac.at/2013/competition2013.pdf Report]

* [[Termination Competition 2012]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=362062 Results], [http://verify.rwth-aachen.de/giesl/competition2012.pdf Report]

* [[Termination Competition 2011]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=230715 Results], [http://termcomp.uibk.ac.at/2011/competition2011.pdf Report]

* [[Termination Competition 2010]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=185404 Results]

* Termination Competition 2009 [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 Results], [http://lists.lri.fr/pipermail/termtools/2009-November/000778.html Announcement]

* [[Termination_Competition_2008|Termination Competition 2008]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 Results], [http://www.imn.htwk-leipzig.de/~waldmann/talk/09/wst/ Report]
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007], [http://www.imn.htwk-leipzig.de/~waldmann/talk/07/wst/competition/ Report]
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006], [http://www.lri.fr/~marche/termination-competition/2006/reportCompetition2006.pdf Report]
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005], [http://www.lri.fr/~marche/termination-competition/2005/TC.ppt Report]
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004], [http://www.lri.fr/~marche/termination-competition/2004/slides-1jun2004.ps Report]

At the "tool demonstration" in 2003, participating provers (including AProVe, Torpa, Matchbox)
were run on the laptop computers of their developers in the room. Termination problems were announced
on the spot by participants, then written on the blackboard, then typed in by everyone, and when a team's program
could solve it, they shouted "solved".

== Results ==

The results of (almost) all competitions are available [https://termcomp.github.io/ here]

Termination Competition

2026-03-08T12:39:38Z

JCKassing: Simplified the competition page and moved important parts to the top

Termination Competition History

2026-03-08T12:36:50Z

JCKassing: Added an additional page for the history of the termination competition

Termination Competition

2026-03-08T12:33:20Z

JCKassing: Added explanations for each of the category types

= Annual International Termination Competition =

During the 90's a number of new, powerful termination methods
was developed. Thus, at the beginning of the millennium
many research groups started to develop [[:Category:Tools | tools for fully-automated termination analysis]].

After a tool demonstration at the Termination Workshop 2003 (Valencia),
the community then decided to install an annual termination competition, and to collect benchmarks,
to spur the development of tools and new termination techniques.

== Upcoming Competitions ==

* The [[Termination Competition 2025]] will be held during [https://www.imn.htwk-leipzig.de/WST2025/ WST 2025], September 3-4, Leipzig, Germany.

== Organization ==

Questions and suggestions regarding the competition
should go to [[Termtools|the termtools mailing list]].
Discussion is open and happens primarily on the list.
Decisions will be made by votes among the [[Termination Competition Steering Committee]], with current members
* [https://ffrohn.github.io Florian Frohn] (Chair), RWTH Aachen
* [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen
* [http://cl-informatik.uibk.ac.at/users/georg/ Georg Moser], University of Innsbruck
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], Université de La Réunion
* [https://group-mmm.org/~ayamada/ Akihisa Yamada], AIST Tokyo Waterfront
* Dieter Hofbauer, ASW Saarland

From 2004 till 2007, the competition organizer was Claude Marché, [http://www.lri.fr/~marche/termination-competition/ Paris].
From 2008 to 2013 the competition was run by René Thiemann, [http://termcomp.uibk.ac.at Innsbruck].
From 2014 to 2017, the competition organizer was Johannes Waldmann. Jobs were run on the [https://www.starexec.org/ Star Exec] platform at U Iowa.
From 2018 to 2023, the organizer was Akihisa Yamada.
From 2024 on, the organizer is Florian Frohn.

== Competition Categories ==

Currently, the competition features the following categories. Since 2007 some of the categories also have [[Certified_Termination|certified categories]], where an additional certifier checks the output of the tools. Categories that were used in the past but not included in the three most recent competitions are marked with an ✖.

=== Termination of Rewriting ===

These categories consider the termination of rewrite systems, a foundational computational model used to represent symbolic computation and program transformations.
The goal is to automatically prove that no infinite rewrite sequences are possible for the given system.
Different categories capture variations of rewriting such as relative rewriting, context-sensitive rewriting, conditional rules, or restrictions on the rewriting strategy (e.g., innermost or outermost rewriting).

<div style="column-count:3; column-gap:2em;">
* [[Term Rewriting#TRS Standard|TRS Standard]]
* [[Term Rewriting#TRS Relative|TRS Relative]]
* [[Term Rewriting#TRS Contextsensitive|TRS Contextsensitive]]
* [[Term Rewriting#TRS Equational|TRS Equational]]
* [[Term Rewriting#TRS Innermost|TRS Innermost]]
* [[Term Rewriting#TRS Outermost|TRS Outermost]]
* [[Term Rewriting#TRS Conditional|TRS Conditional]]
* [[Term Rewriting#TRS Conditional - Operational Termination|TRS Conditional - Operational Termination]]
* [[Term Rewriting#SRS Standard|SRS Standard]]
* [[Term Rewriting#SRS Relative|SRS Relative]]
* [[Cycle_Rewriting|Cycle Rewriting]] ✖
* [[Higher_Order|Higher Order Rewriting]] (since 2010)
* [[ITRS|ITRS Innermost]] (since 2014)
* [[Term Rewriting#Integer Transition Systems|ITS]] (since 2014)
</div>

=== Termination of Probabilistic Rewriting ===

These categories address probabilistic rewrite systems , where rewrite rules are applied according to probability distributions.
Instead of classical termination, the goal is to prove almost-sure termination, i.e., that infinite executions occur with probability zero,
or strong almost-sure termination, i.e., that the expected runtime is finite.
This lifts termination analysis to models that capture randomized algorithms or stochastic behavior.

<div style="column-count:3; column-gap:2em;">
* [[Probabilistic Rewriting#PTRS Standard|PTRS Standard]] (since 2024)
* [[Probabilistic Rewriting#PTRS Innermost|PTRS Innermost]] (since 2024)
</div>

Currently, there are only categories regarding probabilistic rewrite systems,
but an extension to probabilistic imperative programs may be possible in future competitions.

=== Termination of Programs ===

These categories focus on proving termination of actual programming languages used in industry.
The categories differ by the source programming language or program model.

<div style="column-count:3; column-gap:2em;">
* [[Logic_Programming|Termination of logic programs]]
* [[Functional_Programming|Termination of functional programs]] (since 2007)
* [[Java_Bytecode|Termination of Java Bytecode programs]] (since 2009)
* [[C_Programs|Termination of C programs]] (since 2014)
</div>

=== Complexity of Rewriting ===

These categories evaluate tools that automatically analyze the asymptotic complexity of rewrite systems .
Instead of only proving termination, the goal is to derive upper bounds on the length of rewrite sequences,
typically expressed as functions of the input size.
Different categories measure difference runtime complexities under various rewriting strategies and different restrictions on the initial start term.

<div style="column-count:3; column-gap:2em;">
* [[Term Rewriting#Runtime Complexity|TRS Runtime Complexity]]
* [[Term Rewriting#Runtime Complexity|TRS Innermost Runtime Complexity]]
* [[Term Rewriting#Runtime Complexity|TRS Derivational Complexity]]
* [[Term Rewriting#Runtime Complexity|TRS Innermost Derivational Complexity]]
* TRS Parallel Innermost Derivational Complexity
* [[Term Rewriting#Integer Transition Systems|ITS Complexity]]
</div>

=== Complexity Analysis ===

These categories focus on automatically determining time complexity bounds for programs written in concrete programming languages .
Tools analyze the program’s control flow, data dependencies, and loops to derive asymptotic upper bounds on runtime with respect to the input size.

<div style="column-count:3; column-gap:2em;">
* [[C_Complexity|Complexity of C programs]]
</div>

== Termination Problems Data Base ==

The [[TPDB|Termination Problems Data Base]] collects all the problems used in the competitions.

We welcome problem submissions from non-participants.

== History of Termination Competitions ==

The following competitions have taken place:

* [[Termination Competition 2025]] affiliated with [https://www.imn.htwk-leipzig.de/WST2025/ WST 2025], [https://termcomp.github.io/Y2025/ Results].
* [[Termination Competition 2024]] affiliated with [https://merz.gitlabpages.inria.fr/2024-ijcar/ IJCAR 2024], [https://termcomp.github.io/Y2024/ Results].
* [[Termination Competition 2023]] affiliated with [[WST2023]], [https://termcomp.github.io/Y2023/ Results].
* [[Termination Competition 2022]] affiliated with [https://easychair.org/smart-program/FLoC2022/IJCAR-index.html IJCAR 2022], [https://termcomp.github.io/Y2022/ Results].
* [[Termination Competition 2021]] affiliated with [http://www.cs.cmu.edu/~mheule/CADE28/ CADE 2021], [https://termcomp.github.io/Y2021/ Results].
* [[Termination Competition 2020]] affiliated with [https://ijcar2020.org/ IJCAR 2020], [https://termcomp.github.io/Y2020/ Results].
* [[Termination Competition 2019]] affiliated with [https://tacas.info/toolympics.php Toolympics at TACAS 2019], [https://termcomp.github.io/Y2019/ Results].
* [[Termination Competition 2018]] affiliated with FLoC 2018, Oxford, UK, July 13, 2018, [https://termcomp.github.io/Y2018/ Results].

* [[Termination_Competition_2017|Termination Competition 2017]] affiliated with [http://www.cs.ox.ac.uk/conferences/fscd2017/ FSCD], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2017 Results of Competition], [http://termcomp.imn.htwk-leipzig.de/competitions/67 Results of demonstration].

* [[Termination_Competition_2016|Termination Competition 2016]] affiliated with [http://cl-informatik.uibk.ac.at/events/wst-2016/ WST (Workshop on Termination)], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2016 Results of Competition]. [http://www.cs.upc.edu/~albert/papers/termcomp2016_slides.pdf Presentation at WST]

* [[Termination Competition 2015]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2015 Results of Competition], [http://www.cs.upc.edu/~albert/papers/termCompCADE2015.pdf Description paper at CADE-25] [http://www.cs.upc.edu/~albert/papers/termcomp2015_slides.pdf Report]

* [[Termination Competition 2014]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2014 Results of Competition], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/23 Results of Demonstration]

* [[Termination Competition 2013]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=437763 Results], [http://termcomp.uibk.ac.at/2013/competition2013.pdf Report]

* [[Termination Competition 2012]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=362062 Results], [http://verify.rwth-aachen.de/giesl/competition2012.pdf Report]

* [[Termination Competition 2011]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=230715 Results], [http://termcomp.uibk.ac.at/2011/competition2011.pdf Report]

* [[Termination Competition 2010]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=185404 Results]

* Termination Competition 2009 [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 Results], [http://lists.lri.fr/pipermail/termtools/2009-November/000778.html Announcement]

* [[Termination_Competition_2008|Termination Competition 2008]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 Results], [http://www.imn.htwk-leipzig.de/~waldmann/talk/09/wst/ Report]
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007], [http://www.imn.htwk-leipzig.de/~waldmann/talk/07/wst/competition/ Report]
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006], [http://www.lri.fr/~marche/termination-competition/2006/reportCompetition2006.pdf Report]
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005], [http://www.lri.fr/~marche/termination-competition/2005/TC.ppt Report]
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004], [http://www.lri.fr/~marche/termination-competition/2004/slides-1jun2004.ps Report]

At the "tool demonstration" in 2003, participating provers (including AProVe, Torpa, Matchbox)
were run on the laptop computers of their developers in the room. Termination problems were announced
on the spot by participants, then written on the blackboard, then typed in by everyone, and when a team's program
could solve it, they shouted "solved".

== Results ==

The results of (almost) all competitions are available [https://termcomp.github.io/ here]

Tools:AProVE

2026-03-06T22:23:03Z

JCKassing: Changed the developer list to the current website list

{{Tool
|shortname=AProVE
|longname=Automated Program Verification Environment
|homepage=http://aprove.informatik.rwth-aachen.de
|country=Germany
|university=RWTH Aachen
|developers=https://aprove.informatik.rwth-aachen.de/contact
|publication=[[Bibtex:AProVE14|Proving Termination of Programs Automatically with AProVE]]
}}



[[File:Aprove_logo_new.png|400px|thumb|center|AProVE logo]]

Termination Competition

2026-02-24T15:10:03Z

JCKassing: Improved the categorization of all competition categories

= Annual International Termination Competition =

During the 90's a number of new, powerful termination methods
was developed. Thus, at the beginning of the millennium
many research groups started to develop [[:Category:Tools | tools for fully-automated termination analysis]].

After a tool demonstration at the Termination Workshop 2003 (Valencia),
the community then decided to install an annual termination competition, and to collect benchmarks,
to spur the development of tools and new termination techniques.

== Upcoming Competitions ==

* The [[Termination Competition 2025]] will be held during [https://www.imn.htwk-leipzig.de/WST2025/ WST 2025], September 3-4, Leipzig, Germany.

== Organization ==

Questions and suggestions regarding the competition
should go to [[Termtools|the termtools mailing list]].
Discussion is open and happens primarily on the list.
Decisions will be made by votes among the [[Termination Competition Steering Committee]], with current members
* [https://ffrohn.github.io Florian Frohn] (Chair), RWTH Aachen
* [https://verify.rwth-aachen.de/giesl/ Jürgen Giesl], RWTH Aachen
* [http://cl-informatik.uibk.ac.at/users/georg/ Georg Moser], University of Innsbruck
* [http://lim.univ-reunion.fr/staff/epayet/ Étienne Payet], Université de La Réunion
* [https://group-mmm.org/~ayamada/ Akihisa Yamada], AIST Tokyo Waterfront
* Dieter Hofbauer, ASW Saarland

From 2004 till 2007, the competition organizer was Claude Marché, [http://www.lri.fr/~marche/termination-competition/ Paris].
From 2008 to 2013 the competition was run by René Thiemann, [http://termcomp.uibk.ac.at Innsbruck].
From 2014 to 2017, the competition organizer was Johannes Waldmann. Jobs were run on the [https://www.starexec.org/ Star Exec] platform at U Iowa.
From 2018 to 2023, the organizer was Akihisa Yamada.
From 2024 on, the organizer is Florian Frohn.

== Competition Categories ==

Currently, the competition features the following categories. Since 2007 some of the categories also have [[Certified_Termination|certified categories]], where an additional certifier checks the ouput of the tools. Categories that were used in the past but not included in the three most recent competitions are marked with an ✖.

=== Termination of Rewriting ===

<div style="column-count:3; column-gap:2em;">
* [[Term Rewriting#TRS Standard|TRS Standard]]
* [[Term Rewriting#TRS Relative|TRS Relative]]
* [[Term Rewriting#TRS Contextsensitive|TRS Contextsensitive]]
* [[Term Rewriting#TRS Equational|TRS Equational]]
* [[Term Rewriting#TRS Innermost|TRS Innermost]]
* [[Term Rewriting#TRS Outermost|TRS Outermost]]
* [[Term Rewriting#TRS Conditional|TRS Conditional]]
* [[Term Rewriting#TRS Conditional - Operational Termination|TRS Conditional - Operational Termination]]
* [[Term Rewriting#SRS Standard|SRS Standard]]
* [[Term Rewriting#SRS Relative|SRS Relative]]
* [[Cycle_Rewriting|Cycle Rewriting]] ✖
* [[Higher_Order|Higher Order Rewriting]] (since 2010)
* [[ITRS|ITRS Innermost]] (since 2014)
* [[Term Rewriting#Integer Transition Systems|ITS]] (since 2014)
</div>

=== Termination of Probabilistic Rewriting ===

<div style="column-count:3; column-gap:2em;">
* [[Probabilistic Rewriting#PTRS Standard|PTRS Standard]] (since 2024)
* [[Probabilistic Rewriting#PTRS Innermost|PTRS Innermost]] (since 2024)
</div>

=== Termination of Programs ===

<div style="column-count:3; column-gap:2em;">
* [[Logic_Programming|termination of logic programs]]
* [[Functional_Programming|termination of functional programs]] (since 2007)
* [[Java_Bytecode|termination of Java Bytecode programs]] (since 2009)
* [[C_Programs|termination of C programs]] (since 2014)
</div>

=== Complexity of Rewriting ===

<div style="column-count:3; column-gap:2em;">
* [[Term Rewriting#Runtime Complexity|TRS Runtime Complexity]]
* [[Term Rewriting#Runtime Complexity|TRS Innermost Runtime Complexity]]
* [[Term Rewriting#Runtime Complexity|TRS Derivational Complexity]]
* [[Term Rewriting#Runtime Complexity|TRS Innermost Derivational Complexity]]
* TRS Parallel Innermost Derivational Complexity
* [[Term Rewriting#Integer Transition Systems|ITS Complexity]]
</div>

=== Complexity Analysis ===

<div style="column-count:3; column-gap:2em;">
* [[C_Complexity|Complexity of C programs]]
</div>

== Termination Problems Data Base ==

The [[TPDB|Termination Problems Data Base]] collects all the problems used in the competitions.

We welcome problem submissions from non-participants.

== History of Termination Competitions ==

The following competitions have taken place:

* [[Termination Competition 2025]] affiliated with [https://www.imn.htwk-leipzig.de/WST2025/ WST 2025], [https://termcomp.github.io/Y2025/ Results].
* [[Termination Competition 2024]] affiliated with [https://merz.gitlabpages.inria.fr/2024-ijcar/ IJCAR 2024], [https://termcomp.github.io/Y2024/ Results].
* [[Termination Competition 2023]] affiliated with [[WST2023]], [https://termcomp.github.io/Y2023/ Results].
* [[Termination Competition 2022]] affiliated with [https://easychair.org/smart-program/FLoC2022/IJCAR-index.html IJCAR 2022], [https://termcomp.github.io/Y2022/ Results].
* [[Termination Competition 2021]] affiliated with [http://www.cs.cmu.edu/~mheule/CADE28/ CADE 2021], [https://termcomp.github.io/Y2021/ Results].
* [[Termination Competition 2020]] affiliated with [https://ijcar2020.org/ IJCAR 2020], [https://termcomp.github.io/Y2020/ Results].
* [[Termination Competition 2019]] affiliated with [https://tacas.info/toolympics.php Toolympics at TACAS 2019], [https://termcomp.github.io/Y2019/ Results].
* [[Termination Competition 2018]] affiliated with FLoC 2018, Oxford, UK, July 13, 2018, [https://termcomp.github.io/Y2018/ Results].

* [[Termination_Competition_2017|Termination Competition 2017]] affiliated with [http://www.cs.ox.ac.uk/conferences/fscd2017/ FSCD], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2017 Results of Competition], [http://termcomp.imn.htwk-leipzig.de/competitions/67 Results of demonstration].

* [[Termination_Competition_2016|Termination Competition 2016]] affiliated with [http://cl-informatik.uibk.ac.at/events/wst-2016/ WST (Workshop on Termination)], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2016 Results of Competition]. [http://www.cs.upc.edu/~albert/papers/termcomp2016_slides.pdf Presentation at WST]

* [[Termination Competition 2015]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2015 Results of Competition], [http://www.cs.upc.edu/~albert/papers/termCompCADE2015.pdf Description paper at CADE-25] [http://www.cs.upc.edu/~albert/papers/termcomp2015_slides.pdf Report]

* [[Termination Competition 2014]], [http://termcomp.imn.htwk-leipzig.de/competitions/Y2014 Results of Competition], [http://nfa.imn.htwk-leipzig.de/termcomp/competition/23 Results of Demonstration]

* [[Termination Competition 2013]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=437763 Results], [http://termcomp.uibk.ac.at/2013/competition2013.pdf Report]

* [[Termination Competition 2012]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=362062 Results], [http://verify.rwth-aachen.de/giesl/competition2012.pdf Report]

* [[Termination Competition 2011]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=230715 Results], [http://termcomp.uibk.ac.at/2011/competition2011.pdf Report]

* [[Termination Competition 2010]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=185404 Results]

* Termination Competition 2009 [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=101722 Results], [http://lists.lri.fr/pipermail/termtools/2009-November/000778.html Announcement]

* [[Termination_Competition_2008|Termination Competition 2008]], [http://termcomp.uibk.ac.at/termcomp/competition/competitionSummary.seam?comp=15991 Results], [http://www.imn.htwk-leipzig.de/~waldmann/talk/09/wst/ Report]
* [http://www.lri.fr/~marche/termination-competition/2007/ Termination Competition 2007], [http://www.imn.htwk-leipzig.de/~waldmann/talk/07/wst/competition/ Report]
* [http://www.lri.fr/~marche/termination-competition/2006/ Termination Competition 2006], [http://www.lri.fr/~marche/termination-competition/2006/reportCompetition2006.pdf Report]
* [http://www.lri.fr/~marche/termination-competition/2005/ Termination Competition 2005], [http://www.lri.fr/~marche/termination-competition/2005/TC.ppt Report]
* [http://www.lri.fr/~marche/termination-competition/2004/ Termination Competition 2004], [http://www.lri.fr/~marche/termination-competition/2004/slides-1jun2004.ps Report]

At the "tool demonstration" in 2003, participating provers (including AProVe, Torpa, Matchbox)
were run on the laptop computers of their developers in the room. Termination problems were announced
on the spot by participants, then written on the blackboard, then typed in by everyone, and when a team's program
could solve it, they shouted "solved".

== Results ==

The results of (almost) all competitions are available [https://termcomp.github.io/ here]

People:Jan-Christoph Kassing

2026-01-15T12:44:22Z

JCKassing: Added profile pic

{{Person
|firstname=Jan-Christoph
|middlenames=
|lastname=Kassing
|titles=
|email=Kassing@cs.rwth-aachen.de
|homepage=http://jckassing.com/
|country=Germany
|university=RWTH Aachen
|department=Research Group Computer Science 2
|role=PhD Student 
}}



[https://jckassing.com/ https://jckassing.com/images/Kassing_close.png]

Category:Categories

2026-01-15T12:42:43Z

JCKassing: Improving Category text

The tools developed by the community address different types of problems.
This page lists all problem categories supported by tools in the Termination Portal.
Each category represents a class of programs together with a specific analysis goal,
such as proving termination or deriving upper bounds on the runtime complexity.

Probabilistic Rewriting

2026-01-15T12:36:09Z

JCKassing: Added to the category group

People:Jan-Christoph Kassing

2026-01-15T12:33:56Z

JCKassing: Added myself as a person

{{Person
|firstname=Jan-Christoph
|middlenames=
|lastname=Kassing
|titles=
|email=Kassing@cs.rwth-aachen.de
|homepage=http://jckassing.com/
|country=Germany
|university=RWTH Aachen
|department=Research Group Computer Science 2
|role=PhD Student 
}}

People:Jürgen Giesl

2026-01-15T12:27:36Z

JCKassing: Fixed Link

{{Person
|firstname=Jürgen
|middlenames=
|lastname=Giesl
|titles=
|email=giesl@informatik.rwth-aachen.de
|homepage=http://verify.rwth-aachen.de/giesl/
|country=Germany
|university=RWTH Aachen
|department=Research Group Computer Science 2
|role=Professor 
}}



[https://verify.rwth-aachen.de/giesl/ https://verify.rwth-aachen.de/giesl/index-Dateien/Giesl_Small.jpg]

People:Jürgen Giesl

2026-01-15T12:27:13Z

JCKassing: Update Image

{{Person
|firstname=Jürgen
|middlenames=
|lastname=Giesl
|titles=
|email=giesl@informatik.rwth-aachen.de
|homepage=http://verify.rwth-aachen.de/giesl/
|country=Germany
|university=RWTH Aachen
|department=Research Group Computer Science 2
|role=Professor 
}}



[https://verify.rwth-aachen.de/giesl/index-Dateien/ https://verify.rwth-aachen.de/giesl/index-Dateien/Giesl_Small.jpg]

Probabilistic Rewriting

2026-01-15T11:19:07Z

JCKassing: some additional information on the probabilistic rewriting site

Termination Competition 2025 technical details

2025-07-23T13:20:06Z

JCKassing: /* Testing Locally */

== Execution Environment ==

Starting from 2025, TermComp runs on the RWTH HPC cluster.

Tools must be submitted as Docker images. The competition will run using Apptainer (which can run Docker images). During the competition, the following two commands will be executed in your container:

* solver --name
* solver --timeout=$timeout --category=$category $benchmark

So an executable named "solver" must be available in your container.
The former command must print the name of your solver to stdout.
The latter must analyze the provided $benchmark w.r.t.\ the rules of the given $category, taking the given $timeout into account.

A list with the exact category names will be published before the competition.
They will essentially be identical to the names of the corresponding TPDB directories.

== Testing Locally ==

* Install [https://apptainer.org/docs/admin/main/installation.html Apptainer].
* Build and tag your docker image locally. In my case, its full name is loat/loat-termcomp:445e86.
* Convert your docker image to an Apptainer image via
<code>apptainer build $apptainer_image.sif docker-daemon://$docker_image</code>
 
So in my case, the full command is
 
<code>apptainer build loat.sif docker-daemon:loat/loat-termcomp:445e86</code>
* First test
<code>
apptainer exec $apptainer_image.sif solver --name
</code>

In my case, I get:

<code>
apptainer exec loat.sif solver --name

LoAT
</code>
* Then test
<code>
apptainer exec solver --timeout=60 --category=$category $benchmark
</code>

In my case, I get:

<code>
apptainer exec loat.sif solver --timeout=60 --category=Integer_Transition_Systems TPDB/Integer_Transition_Systems/From_AProVE_2014/Velroyen08-alternDiv.jar-obl-8.smt2

NO
</code>

== Lessons Learned from Testing ==

=== General ===

* The image must be for an '''amd64-architecture'''.

=== Docker - Apptainer incompatibilities ===

The following things must be taken into account if you submit a Docker image.

* The solver-command must behave as intended '''for all users''', not just for a specific one.
* The solver-command must behave as intended '''independently from the current working directory'''.

== Registration ==

To register, you need to create a pull request for [https://github.com/TermCOMP/registration this repository].
More specifically, to register for a certain $category, checkout the branch for the corresponding competition (e.g., the branch 2025 for termCOMP '25) and add a line to $category.txt.
The content of the line must be the identifier of your Docker image on [https://hub.docker.com/ Docker Hub], so that it can directly be passed to "docker pull".

Term Rewriting

2024-05-13T13:17:47Z

JCKassing:

== General ==

We use an adaption of the [https://project-coco.uibk.ac.at/ARI/ ARI format], so TRSs are represented as S-Expressions (see [https://smt-lib.org/papers/smt-lib-reference-v2.6-r2021-05-12.pdf here, Sec. 3.1]). Our format differs from the format used at CoCo as follows:

* We do not impose any variable conditions, so a rewrite rule is a pair of arbitrary terms.
* Identifiers must be valid SMT-LIB symbols (see [https://smt-lib.org/papers/smt-lib-reference-v2.6-r2021-05-12.pdf here, Sec. 3.2]), whereas CoCo uses a more liberal definition. Both simple and quoted symbols are allowed. As in SMT-LIB, simple symbols must not be equal to reserved words. In our case, the reserved words are: <pre>fun, rule, format, sort, theory, define-fun, prule</pre> To ease parsing, we impose the following additional restrictions:
** Quoted identifiers must be non-empty.
** Quoted identifiers must not contain whitespace, parantheses, or semicolons.
** All occurrences of the same identifier must be either quoted or unquoted. So <pre>(rule |a| |a|)</pre> is valid, but <pre>(rule a |a|)</pre> is invalid.
* Rules are annotated with optional costs, which are natural numbers. This allows, e.g., to model relative rewriting (by setting the cost of relative rules to 0). Categories may disallow costs. So rules are defined as follows:
<pre>
rule ::= ( rule term term cost? )
cost ::= :cost number
</pre>

In contrast to the former XTC format, the goal of the analysis is implicitly specified by the category.

== Termination ==

All termination categories consider termination w.r.t. arbitrary start terms.

=== Relative Termination ===

All categories for relative termination consider full rewriting.
See [https://project-coco.uibk.ac.at/ARI/trs.php here] for the format of all categories for relative termination.

==== TRS Relative ====

* no further restrictions

==== SRS Relative ====

* just unary function symbols

=== Non-Relative Termination ===

All categories for non-relative termination disallow costs.

==== TRS Standard ====

* full rewriting
* see [https://project-coco.uibk.ac.at/ARI/trs.php here]

==== SRS Standard ====

* full rewriting
* just unary function symbols
* see [https://project-coco.uibk.ac.at/ARI/trs.php here]

==== TRS Contextsensitive ====

* context-sensitive rewriting
* see [https://project-coco.uibk.ac.at/ARI/cstrs.php here]

==== TRS Equational ====

Here, a ''theory'' may be added to declarations of function symbols.

<pre>
fun ::= ( fun identifier number theory? )
theory ::= :theory [A | C | AC]
</pre>

* full rewriting modulo associativity / commutativity / associativity and commutativity

==== TRS Innermost ====

* innermost rewriting
* see [https://project-coco.uibk.ac.at/ARI/trs.php here]

==== TRS Outermost ====

* outermost rewriting
* see [https://project-coco.uibk.ac.at/ARI/trs.php here]

==== TRS Conditional ====

* full conditional rewriting
* see [https://project-coco.uibk.ac.at/ARI/ctrs.php here]
* currently, we only support the condition-type ''oriented''

==== TRS Conditional - Operational Termination ====

* TODO clarify the difference to ''TRS Conditional''
* see [https://project-coco.uibk.ac.at/ARI/ctrs.php here]
* currently, we only support the condition-type ''oriented''

== Complexity ==

See [https://project-coco.uibk.ac.at/ARI/trs.php here] for all complexity categories.

=== Runtime Complexity ===

All categories for runtime complexity consider basic start terms only.

==== Runtime Complexity Innermost ====

* innermost rewriting

==== Runtime Complexity Full ====

* full rewriting

=== Derivational Complexity ===

All categories for derivational complexity consider arbitrary start terms.

==== Derivational Complexity Innermost ====

* innermost rewriting

==== Derivational Complexity Full ====

* full rewriting