left

Techniques working on SCCs

right
AProVE Help SystemTechniquesTechniques working on SCCs
Non Overlappingness Check
Modular Removal of Rules
Solver with Polynomial Order
Solver with Argument Filtering
Size Change Principle
DP Transformations
Rewriting
Narrowing
Instantiation
RFC Matchbounds
Semantic Labelling
Reversal
Subterm
Non-Termination

All the techniques presented here are useful to analyze the absence or existence of infinite dependency pair chains. They do so by investigating the behavior of the strongly connected components (SCCs) of the dependency graph yielded by the dependency pair method.