Equational term rewriting plays a prominent role in many areas of computer science, including specification, verification, and automated reasoning.

In these applications, termination is an important property that is generally assumed to be given. This thesis investigates methods that can be used to analyze the termination behavior of equational term rewriting in a fully automated way.

After presenting methods based on reduction orders, we introduce the powerful dependency pair method that is well suited for automation. The main part of this work presents new improvements of the dependency pair method that significantly increase its efficiency and power in practice.

The results have been implemented in the termination prover AProVE for the two classes of equational theories most commonly found in practice, namely associative-commutative (AC) theories and theories of non-free constructors. There are other systems for automated analysis of AC-termination available, but empirical results indicate that the contributions of this thesis improve upon the previously known techniques in practice. For theories of non-free constructors, AProVE is, to the best of our knowledge, the only system that provides powerful methods for fully automated termination proofs.