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.
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.