left

Solver with Argument Filtering

right
AProVE Help SystemTechniquesTechniques working on SCCsSolver with Argument Filtering

Description

Given an SCC P over a TRS R this techniques tries to find an argument filtering π and a Ce-compatible order > satisfying 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: 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.