§04§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.- VMTL-A Modular Terminatio §04§n 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. §04§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.- VMTL-A Modular Terminatio §04§n 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.