# Integer Term Rewriting

From Termination-Portal.org

(Redirected from ITRS)

The main idea of ITRSs is to add pre-defined constructors for integers (the integers themselves) and Booleans (true / false) and arithmetic, relational and Boolean functions like

+, -, *,/ ,%, >, >=, <, &&, ||, !, ...

to conventional TRSs using the *innermost* rewrite strategy. To this
aim it is necessary to extend the XTC format by the ability to represent
pre-defined semantics for function symbols.
Not only ITRSs, but also other extensions with pre-defined functions can be
represented using this extension of the XTC format. A formal definition of ITRSs and their evaluation can be found
in this paper.