[Back]

M. Hutagalung:
"Proving Termination of Rewriting with the Dependency Pair Framework";
Supervisor: B. Gramlich; Computersprachen (E185) / AB Theoretische Informatik und Logik (E185/2), 2010.

Termination is besides confluence the most important and fundamental
property of term rewriting systems (TRSs). If a TRS is terminating,
then this guarantees that every strategy of computing with the system
will always end with normal forms. But unfortunately, the
undecidability of termination shows that there cannot be an automated
method that will succeed in proving termination of all terminating
TRSs. Numerous syntactical as well as semantical methods have been
developed, but there are still many important TRSs whose termination
cannot be shown. The dependency pair framework (introduced in [AG00]
and generally formulated in [GTS05], shortly called the DP framework)
is currently the most powerful method that can increase significantly
the class of systems where termination is provable automatically. The
power of the framework lies in its high flexibility, due to its
general and modular structure, and the ability to incorporate other
general termination proof methods. This thesis will summarize the DP
framework and its ingredients. First, we summarize the theoretical
foundations of the framework, that allows various dependency pair
processors (DP processors) to successively simplify the initial
termination proof problems. Then, as the main part of the summary, we
will give a comprehensive survey of some important types of DP
processors. The DP processors can be seen as the termination
techniques in the DP framework. All termination proofs in the DP
framework are basically obtained by repeated applications of DP
processors. For each DP processor we work out the basic underlying
ideas and theory, present some refinements, and illustrate their
applications by examples. In addition, we will also include a short
survey of some general termination proof methods, e.g. reduction
orders (polynomial interpretations, matrix interpretations,
simplification orders), match-bounds, and semantic labeling, which can
also be applied within the DP framework.

http://publik.tuwien.ac.at/files/PubDat_194745.pdf