|
Subterm |
|
Description
Given an SCC P over a TRS R this techniques tries to find a (collapsing) argument filter
π working only on tuple symbols such that
- π(s) ≥ π(t) for all DPs s → t ∈ P
- π(s) > π(t) for at least one DP s → t ∈ P
Here, > denotes the subterm relation.
If such an argument filter is found, all strictly decreasing
DPs are removed from P.
After the removal the Dependency Graph for the remaining DPs is computed again.
The set of SCCs of this new graph is the final result of this technique.
See [HM '04] for references.
Application and Configuration
There is nothing to configure here.
The method is fast but only of limited power.
The usual solver
with argument filtering used with the embedding order is on natural
examples not much slower but more powerful than this technique.