Rewriting Techniques and Applications: 15th International Conference, RTA 2004, Aachen, Germany, June 3-5, 2004, Proceedings (Lecture Notes in Computer Science (3091))

this Book Constitutes The Refereed Proceedings Of The 15th International Conference On Rewriting Techniques And Applications, Rta 2004, Held In Aachen, Germany In June 2004. Front Matter....Pages - Termination Analysis of the Untyped λ -Calculus....Pages 1-23 A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems....Pages 24-39 Termination of S-Expression Rewriting Systems: Lexicographic Path Ordering for Higher-Order Terms....Pages 40-54 Monadic Second-Order Unification Is NP-Complete....Pages 55-69 A Certified AC Matching Algorithm....Pages 70-84 Matchbox : A Tool for Match-Bounded String Rewriting....Pages 85-94 TORPA: Termination of Rewriting Proved Automatically....Pages 95-104 Querying Unranked Trees with Stepwise Tree Automata....Pages 105-118 A Verification Technique Using Term Rewriting Systems and Abstract Interpretation....Pages 119-133 Rewriting for Fitch Style Natural Deductions....Pages 134-154 Efficient λ -Evaluation with Interaction Nets....Pages 155-169 Proving Properties of Term Rewrite Systems via Logic Programs....Pages 170-184 On the Modularity of Confluence in Infinitary Term Rewriting....Pages 185-199 mu-term : A Tool for Proving Termination of Context-Sensitive Rewriting....Pages 200-209 Automated Termination Proofs with AProVE ....Pages 210-220 An Approximation Based Approach to Infinitary Lambda Calculi....Pages 221-232 Böhm-Like Trees for Term Rewriting Systems....Pages 233-248 Dependency Pairs Revisited....Pages 249-268 Inductive Theorems for Higher-Order Rewriting....Pages 269-284 The Joinability and Unification Problems for Confluent Semi-constructor TRSs....Pages 285-300 A Visual Environment for Developing Context-Sensitive Term Rewriting Systems....Pages 301-311 Back Matter....Pages - This volume contains the proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA 2004), which was held June 2- 5, 2004, at the RWTH Aachen in Germany. RTA is the major forum for the presentation of research on all aspects of rewriting. Previous RTA conferences took place in Dijon (1985), Bordeaux (1987), Chapel Hill (1989), Como (1991), Montreal (1993), Kaiserslautern (1995), Rutgers (1996), Sitges (1997), Tsukuba (1998), Trento (1999), Norwich (2000), Utrecht (2001), Copenhagen (2002), and Valencia (2003). The program committee selected 19 papers for presentation, including ?ve system descriptions, from a total of 43 submissions. In addition, there were invited talks by Neil Jones, Aart Middeldorp, and Robin Milner. Many people helped to make RTA 2004 a success. I am grateful to the m- bers of the program committee and the external referees for reviewing the s- missionsandmaintainingthehighstandardsoftheRTAconferences. Itisagreat pleasure to thank the conference chair Jurgen ̈ Giesl and the other members of the local organizing committee. They were in charge of the local organization of all events partaking in the Federated Conference on Rewriting, Deduction, and Programming (RDP). Apart from RTA 2004, these events were: - 2nd International Workshop on Higher-Order Rewriting (Delia Kesner, Femke van Raamsdonk, and Joe Wells), - 5th International Workshop on Rule-Based Programming (Slim Abdennadher and Christophe Ringeissen), - 13thInternationalWorkshoponFunctionaland(Constraint)LogicProgr- ming (Herbert Kuchen), - IFIP Working Group 1 The size-change analysis of [5] can show termination of first-order functional programs whose parameter values have a well-founded size order.