6th International School on Rewriting >> Termination of Rewriting: Foundations and Automation

6th International School on Rewriting

July 16th - 20th, 2012. Valencia, Spain


TFA: Termination of Rewriting: Foundations and Automation


Termination is a key property for rewriting. It is not only important when rewriting is used as a model of computation, but also to check other general properties of term rewrite systems like, for instance, confluence. Termination of rewriting is closely related to the concept of well-founded orderings. In fact, until the late 90's, most methods to prove termination automatically used directly reduction orderings, a particular class of well-founded term orderings. From that point on, new methods based on transforming the termination problem into a constraint handling problem were developed, being the Dependency Pair method the most successful approach so far. Many powerful automatic tools have been developed in the last years, making implementation issues an important part of the research in the area.

The course will contain the following topics:

  • Part I. Basic concepts:
    • Termination and well-founded orderings.
    • Orderings on multisets and sequences.
    • Reduction orderings.
    • Interpretation based orderings.
    • Path Orderings.
    • Implementation issues.
  • Part II. Constraint based methods:
    • The dependency pair method.
    • The ordering based approach.
    • Constraint transformation framework.
    • Implementation issues.
  • Part III. Extensions:
    • Termination under strategies.
    • Termination of rewriting modulo theories.
    • Termination of higher-order rewriting.
    • Termination of programs.

<< Back to Previous Page.