Rewriting Techniques and Applications: 15th International Conference, RTA 2004, Aachen, Germany, June 3-5, 2004. Proceedings

Neil D. Jones, Nina Bohr (auth.), Vincent van Oostrom (eds.)3540221530, 9783540221531, 9783540259794

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.

---

Table of contents :
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 –