JCKassing: Added ITS Page

2026-03-18T11:40:28Z

Added ITS Page

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

Integer Transition Systems - Revision history

JCKassing: Added ITS Page