Speaker: Hans Zantema (OAS, TU/e)
Title: Recent developments in proving termination of rewriting automatically

Abstract:
Several tools have been developed for proving termination of
rewriting automatically. Since a few years there is an annual
competition comparing the power of various tools. Strong
improvements in this area show up.

Many techniques can be seen as applications of theorems concluding
termination. Typically, several parameters have to be filled in in
such a way that a list of requirements is fulfilled. Until around
one year ago the main approach was to restrict the search space in
a suitable way and elaborate algorithms searching in this space.
The last year a completely different approach came up in several
tools: describe the requirements on the full search space as a
propositional satisfiability problem, and then apply a state of
the art SAT solver. In particular remarkable results have been
achieved in this way by using matrix interpretations.