Techniques used in AProVE 2011

• CpxTrsToCdt
  This is the transformation from TRSs to the corresponding canonical (extended) DT problem.
• CdtUnreachable
  This processor performs a simple preprocessing (similar to the Oops tool) which removes DTs that cannot be reached from basic terms.
• CdtPolyRedPair
  This is the reduction pair processor combined with the usable rule processor. Here, we use reduction pairs based on polynomial orders.
• CdtMatrixRedPair
  This is the reduction pair processor combined with the usable rule processor. Here, we use reduction pairs based on matrix orders. (However, this processor is only used in one single example.)
• CdtGraphRemoveDangling
  This processor is based on the dependency graph. It is an extension of the leaf removal processor.
• CdtGraphSplitRhs
  This is an additional simple processor to benefit from the dependency graph. It splits up DTs that do not occur in any SCC. More precisely, if s -> COM_n(t_1,...,t_n) does not occur in any SCC, it can be replaced by the DTs s -> COM_1(t_1), ..., s -> COM_1(t_n).
• CdtKnowledge
  This is the knowledge propagation processor.
• CdtNarrowing
  This is the narrowing processor.
• CdtGraphRemoveTrailing
  This processor is a special case of the narrowing processor. It is added as an additional processor for efficiency reasons. If a DT s -> COM_n(t_1,...,t_n) contains a term t_i that has no narrowing substitution, then the DT can be replaced by s -> COM_n(t_1,...,t_{i-1},t_{i+1},...,t_n).
• CdtRewriting
  Similar to the narrowing processor, this processor adapts the "rewriting" processor from the DP framework for complexity analysis.
• CdtInstantiation
  Similar to the narrowing processor, this processor adapts the "instantiation" processor from the DP framework for complexity analysis.
• CdtForwardInstantiation
  Similar to the narrowing processor, this processor adapts the "forward instantiation" processor from the DP framework for complexity analysis.
• SIsEmpty
  This technique simply recognizes solved DT problems (where the component S is empty) and finishes the complexity analysis.
• CpxTrsMatchBounds
  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.