Program

Thursday, December 3

Friday, December 4

Abstracts

• Michel Parigot:
Abstract:
• Martin Avanzini: Complexity Analysis by Graph Rewriting
Abstract: Recently, many techniques have been introduced that allow the (automated) classification of the runtime complexity of TRSs. In this talk I show a tight correspondence between the number of steps performed in a given rewrite system and the computational complexity of an implementation of rewriting. For this we use graph rewriting as a first step towards the implementation of term rewriting. As a result we obtain that polynomial (innermost) runtime complexity of TRSs induces polytime computability of the functions defined.
• Andreas Schnabl: The Derivational Complexity Induced by the Dependency Pair Method Revisited
Abstract: In this talk, we give a brief review of the basics of the dependency pair transformation, an important technique in automatic termination proving. We then give an overview of some refinements of this method, and we discuss the upper bounds on the derivational complexity induced by such termination proofs. In many cases, we conclude an upper bound on the derivational complexity that is elementary or primitive recursive in the upper bound induced by the base technique used in conjunction with the dependency pair transformation.
• Fabien Renaud: Preservation of Strong Normalization for a Higher-Order Rewriting System Explicited
Abstract:
• Sarah Winkler: Ordered Multi-Completion and Theorem Proving with Termination Tools
Abstract: When classical Knuth-Bendix completion fails, ordered completion may still allow to derive a ground-complete rewrite system which is sufficient for many applications such as theorem proving. However, the success of an ordered completion run strongly depends on the reduction order supplied as input. This talk describes how the usage of termination tools can replace fixed reduction orders in ordered completion procedures, which extends to multi-completion as proposed by Kondo and Kurihara. The approach can also be applied to equational theorem proving.
• Friedrich Neurauter: On the Relative Power of Polynomials in Proofs of Termination
Abstract: Polynomial interpretations are a useful technique for proving termination of term rewrite systems. They come in various flavours: polynomial interpretations with real, rational and integer coefficients. In 2006, Lucas proved that there are rewrite systems that can be shown polynomially terminating by using polynomial interpretations with real coefficients, but cannot be shown polynomially terminating using polynomials with rational coefficients only. He also proved a similar theorem with respect to the use of rational coefficients versus integer coefficients. In this talk, we present alternative proofs of Lucas' theorems, which are both shorter and simpler than the original proofs.
• Harald Zankl: Derivational Complexity and Polynomial Interpretations
Abstract: In this talk we introduce the first modular approach for proving (polynomial) derivational complexity of term rewrite systems. The underlying idea is general enough such that all known techniques can be integrated and powerful enough such that all these techniques can be combined. Furthermore the results carry over to the stronger notion of runtime complexity.
• Delia Kesner:
Abstract:
• Andreas Schnabl: The Derivational Complexity Induced by the Dependency Pair Method Revisited
Abstract: In this talk, we give a brief review of the basics of the dependency pair transformation, an important technique in automatic termination proving. We then give an overview of some refinements of this method, and we discuss the upper bounds on the derivational complexity induced by such termination proofs. In many cases, we conclude an upper bound on the derivational complexity that is elementary or primitive recursive in the upper bound induced by the base technique used in conjunction with the dependency pair transformation.