**The Dependency Pair Framework: Combining
Techniques for Automated Termination Proofs**

**Abstract. ** The dependency pair approach is one of the most powerful techniques
for automated termination proofs of term rewrite systems.
Up to now, it was regarded as one of several possible methods to
prove termination. In this talk, we show that dependency pairs can
instead be used as a general concept to integrate arbitrary techniques
for termination analysis. In this way, the benefits of different
techniques can be combined and their modularity and power
are increased significantly. We refer to this new concept as the
"dependency pair framework" to distinguish it from the old
"dependency pair approach". Moreover, this framework facilitates
the development of new methods for termination analysis.
To demonstrate this, we present several new techniques
within the dependency pair framework which simplify
termination problems considerably. We implemented
the dependency pair framework in our termination prover
AProVE and evaluated it on large collections of examples.
The talk is based on joint work with Rene Thiemann
and Peter Schneider-Kamp.

**CERES: Cut-Elimination by Resolution**

**Abstract. ** We present a cut-elimination method for Gentzen's LK which is
based on the resolution calculus. The first step consists in a
structural analysis of a proof P of a sequent S and the extraction
of a clause term X(P). X(P) encodes an abstract structure of the
derivations of cut formulas and represents an unsatisfiable set of
clauses C(P). A resolution refutation R of C(P) then serves as a
skeleton of an LK-proof P' of S with only atomic cuts. P' can be
obtained from the resolution refutation R via so-called
projections of the proof P w.r.t. the clauses in C(P). The main
algorithmic advantage of this method called CERES lies in the
potential to integrate efficient theorem provers (constructing the
resolution refutation R). Moreover the clause terms pave the way
for an algebraic analysis and a mathematical comparison of
cut-elimination methods. In particular it can be shown that CERES
asymptotically outperforms a large class of ``traditional''
cut-elimination methods including this of Gentzen.

**TBA**

**How to Fix it: Using Fixpoints in Different Contexts**

**Abstract. ** In this talk we will discuss the expressive power of mu-calculi. We
will concentrate on those that are extensions of propositional modal
logics with a fixpoint operator. We will consider different kinds of
models, from trees and Kripke structures up to traces and
timed systems.
We will begin with the equivalence of the mu-calculus, automata and
monadic second-order logics (MSOL) on infinite binary trees. Such an
equivalence is fundamental because it certifies the right expressive
power of the mu-calculus and automata models. It is also the origin of
an important set of tools used in verification. We will present how
this equivalence generalizes nicely to all Kripke structures. Next, we
will proceed to trace models that are the simplest among so called
non-interleaving models for concurrency. Unlike words, which are linear
orders on events, traces are partial orders on events. The intuition
is that if two events are not ordered then they have happened
concurrently. Once again, after defining a mu-calculus
appropriately we are able to get the equivalence with MSOL and automata
over traces. Finally, we will discuss the real-time setting. The
situation here is more delicate because both the standard automata
model as well as MSOL are undecidable. We will present recent advances
which give a decidable fixpoint calculus but with yet unknown
expressive power.