Techniques used in AProVE 2012

• reduction pair processor
  This is the reduction pair processor combined with the usable rule processor. Here, we use reduction pairs based on polynomial interpretations.
• leaf removal processor
  This processor is based on the dependency graph and removes DTs that correspond to leaves of the graph.
• unreachable DT removal processor
  This processor removes DTs that cannot be reached from basic terms.
• rhs simplification processor
  This processor simplifies non-leaf DTs by removing subterms from their right-hand side. More precisely, if s → COM_n(t₁, ..., t_n ) is a DT where t_i never gives rise to edges in chain trees, then t_i can be removed from the right-hand side COM_n (t₁ , ..., t_n).
• narrowing processor
  This processor replaces DTs by their narrowings.
• knowledge propagation processor
  This processor benefits from situations where we have already investigated the complexity of all predecessors of a DT.
• forward instantiation processor
  Similar to the narrowing processor, this processor adapts the "forward instantiation" processor from the DP framework for complexity analysis.
• match-bounds
  On SRSs, the match-bound technique is often the technique of choice to analyze termination and complexity. Therefore, we also implemented this technique in AProVE (for both SRSs and TRSs).
• instantiation processor
  Similar to the narrowing processor, this processor adapts the "instantiation" processor from the DP framework for complexity analysis.
• rewriting processor
  Similar to the narrowing processor, this processor adapts the "rewriting" processor from the DP framework for complexity analysis.