Given an SCC P over a TRS R this techniques tries to find an argument filtering π and
a Ce-compatible order > satisfying
π(s) ≥ π(t) for all DPs s → t ∈ P
π(s) > π(t) for at least one DP s → t ∈ P (*)
π(l) ≥ π(r) for all rules l → r ∈ U(P,π)
Here U(P,π) are the usable rules of P regarding the argument filtering π.
If such an argument filtering and order 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 [TGSK '04, GTSKF '03] for references.
Application and Configuration
One can choose between different orders and configure these in more detail pressing the
Configure button. Beside the order the user can choose between different heuristics for
the argument filtering. AProVE offers four possibilities:
All tries all possible argument filterings.
Type restricts the search to those argument filterings that all remaining arguments
are of the same type. Here, a polymorphic type inference algorithm is used to assign
each function symbol a certain type.
Collapse restricts the search to collapsing argument filterings.
CollapseNoArg allows all argument filterings of Collapse, but it
additionally includes argument filterings that reduce function symbols to a constant.
In addition to the heuristics, in the interactive mode the user can
configure the argument filtering in detail and thereby see the filtered constraints. The
corresponding dialog is opened when pressing the Select AFS button.
Processing SCCs by solving filtered constraints is powerful, but depending on the order
and the chosen heuristic it may take same time. Selecting the polynomial order (POLO)
should only be done in the interactive mode to see the corresponding constraints. For
the automatic mode it is better to use the specialized
solver with polynomial order. The reason is that the polynomial
order can do an argument filtering on its own and does not need to get filtered constraints from
the outside.