Difference between revisions of "Integer Term Rewriting"
From Termination-Portal.org
Jump to navigationJump to searchm (moved ITRS to Integer Term Rewriting) |
|||
| Line 5: | Line 5: | ||
+, -, *,/ ,%, >, >=, <, &&, ||, !, ... | +, -, *,/ ,%, >, >=, <, &&, ||, !, ... | ||
| − | to conventional TRSs. To this | + | to conventional TRSs using the ''innermost'' rewrite strategy. To this |
aim it is necessary to extend the XTC format by the ability to represent | aim it is necessary to extend the XTC format by the ability to represent | ||
pre-defined semantics for function symbols. | pre-defined semantics for function symbols. | ||
Revision as of 15:58, 17 June 2014
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.
