Rewriting Techniques and Applications

Thisvolumecontainsthepapersofthe20thInternationalConferenceonRewr- ing Techniques and Applications (RTA 2009), which was held from June 29 to July 1, 2009, in Bras ?lia, Brazil as part of the 5th International Conference on Rewriting, Deduction, and Programming (RDP 2009) together with the Int- national Conference on Typed Lambda Calculi and Applications (TLCA 2009), the International School on Rewriting (ISR 2009), the 4th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2009), the 10th Inter- tional Workshop on Rule-Based Programming (RULE 2009), the 8th Inter- tional Workshop on Functional and (Constraint) Logic Programming (WFLP 2009), the 9th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2009), and the annual meeting of the IFIP Working Group 1.6 on term rewriting. RTA is the major forum for the presentation of research on all aspects of rewriting.PreviousRTAconferenceswereheldinDijon(1985),Bordeaux(1987), Chapel Hill (1989), Como (1991), Montreal (1993), Kaiserslautern (1995), R- gers (1996), Sitges (1997), Tsukuba (1998), Trento (1999), Norwich (2000), Utrecht(2001),Copenhagen(2002),Valencia(2003),Aachen(2004),Nara(2005), Seattle (2006), Paris (2007), and Hagenberg (2008).

Inhalt
Automatic Termination.- Loops under Strategies.- Proving Termination of Integer Term Rewriting.- Dependency Pairs and Polynomial Path Orders.- Unique Normalization for Shallow TRS.- The Existential Fragment of the One-Step Parallel Rewriting Theory.- Proving Confluence of Term Rewriting Systems Automatically.- A Proof Theoretic Analysis of Intruder Theories.- Flat and One-Variable Clauses for Single Blind Copying Protocols: The XOR Case.- Protocol Security and Algebraic Properties: Decision Results for a Bounded Number of Sessions.- YAPA: A Generic Tool for Computing Intruder Knowledge.- Well-Definedness of Streams by Termination.- Modularity of Convergence in Infinitary Rewriting.- A Heterogeneous Pushout Approach to Term-Graph Transformation.- An Explicit Framework for Interaction Nets.- Dual Calculus with Inductive and Coinductive Types.- Comparing Böhm-Like Trees.- The Derivational Complexity Induced by the Dependency Pair Method.- Local Termination.- VMTLA Modular Termination Laboratory.- Tyrolean Termination Tool 2.- From Outermost to Context-Sensitive Rewriting.- A Fully Abstract Semantics for Constructor Systems.- The -Completeness of Most of the Properties of Rewriting Systems You Care About (and Productivity).- Unification in the Description Logic .- Unification with Singleton Tree Grammars.- Unification and Narrowing in Maude 2.4.