|
Techniques working on TRSs |
|
All the techniques presented here are useful to prove or disprove (innermost)
termination of an (equational) TRS. Here, a TRS must not be conditional or
context-sensitive. Furthermore, it is not possible to combine innermost with equational.
Most of the techniques working on TRSs are fast but not very powerful, so these techniques
should be used as a preprocessing.
In order to become really powerful one should use Dependency Pairs
and the corresponding techniques that work on SCCs of the Dependency Graph.