5. RTA 1993: Montreal, Canada

• Leo Bachmair:
  Rewrite Techniques in Theorem Proving (Abstract). 1
  
• Christopher Lynch, Wayne Snyder:
  Redundancy Criteria for Constrained Completion. 2-16
  
• Jordi Levy, Jaume Agustí-Cullell:
  Bi-rewriting, a Term Rewriting Technique for Monotonic Order Relations. 17-31
  
• Hantao Zhang:
  A Case Study of Completion Modulo Distributivity and Abelian Groups. 32-46
  
• Andreas Werner:
  A Semantic Approach to Order-Sorted Rewriting. 47-61
  
• Jürgen Avenhaus, Jörg Denzinger:
  Distributing Equational Theorem Proving. 62-76
  
• Soumen Chakrabarti, Katherine A. Yelick:
  On the Correctness of a Distributed Memory Gröbner basis Algorithm. 77-91
  
• Max Moser:
  Improving Transformation Systems for General E-Unification. 92-105
  
• Joachim Niehren, Andreas Podelski, Ralf Treinen:
  Equational and Membership Constraints for Finite Trees. 106-120
  
• Rolf Backofen:
  Regular Path Expression in Feature Logic. 121-135
  
• Jean H. Gallier:
  Proving Properties of Typed Lambda Terms: Realizability, Covers, and Sheaves (Abstract). 136
  
• Daniel J. Dougherty:
  Some Lambda Calculi with Categorial Sums and Products. 137-151
  
• Andrea Asperti, Cosimo Laneve:
  Paths, Computations and Labels in the Lambda-Calculus. 152-167
  
• Femke van Raamsdonk:
  Confluence and Superdevelopments. 168-182
  
• Zena M. Ariola:
  Relating Graph and Term Rewriting via Böhm Models. 183-197
  
• Nachum Dershowitz, Charles Hoot:
  Topics in Termination. 198-212
  
• Maria C. F. Ferreira, Hans Zantema:
  Total Termination of Term Rewriting. 213-227
  
• Aart Middeldorp, Bernhard Gramlich:
  Simple Termination is Difficult. 228-242
  
• Zurab Khasidashvili:
  Optimal Normalization in Orthogonal Term Rewriting Systems. 243-258
  
• John Field:
  A Graph Reduction Approach to Incremental Term Rewriting (Preliminary Report). 259-273
  
• Ernst Lippe:
  Generating Tables for Bottom-Up Matching. 274-288
  
• Sergei I. Adian:
  On some Algorithmic Problems for Groups and Monoids. 289-300
  
• Franz Baader, Klaus U. Schulz:
  Combination Techniques and Decision Problems for Disunification. 301-315
  
• Mohamed Tajine:
  The Negation Elimination from Syntactic Equational Formula is Decidable. 316-327
  
• Anne-Cécile Caron, Jean-Luc Coquidé, Max Dauchet:
  Encompassment Properties and Automata with Constraints. 328-342
  
• Jean-Claude Raoult:
  Recursively Defined Tree Transductions. 343-357
  
• Maribel Fernández:
  AC Complement Problems: Satisfiability and Negation Elimination. 358-373
  
• Albert Rubio, Robert Nieuwenhuis:
  A Precedence-Based Total AC-Compatible Ordering. 374-388
  
• Catherine Delor, Laurence Puel:
  Extension of the Associative Path Ordering to a Chain of Associative Commutative Symbols. 389-404
  
• David A. Plaisted:
  Polynomial Time Termination and Constraint Satisfaction Tests. 405-420
  
• Ursula Martin:
  Linear Interpretations by Counting Patterns. 421-433
  
• Géraud Sénizergues:
  Some Undecidable Termination Problems for Semi-Thue Systems (Abstract). 434
  

System Description

• Pilar Nivela, Robert Nieuwenhuis:
  Saturation of First-Order (Constrained) Clauses with the Saturate System. 436-440
  
• Brian Matthews:
  MERILL: An Equational Reasoning System in Standard ML. 441-445
  
• Reinhard Bündgen:
  Reduce the Redex -> ReDuX. 446-450
  
• Michael Löwe, Martin Beyer:
  AGG - An Implementation of Algebraic Graph Rewriting. 451-456
  
• Rakesh M. Verma:
  Smaran: A Congruence-Closure Based System for Equational Computations. 457-461
  
• Yexuan Gui, Mitsuhiro Okada:
  LAMBDALG: Higher Order Algebraic Specification Language. 462-466
  

Open Problems

• Nachum Dershowitz, Jean-Pierre Jouannaud, Jan Willem Klop:
  More Problems in Rewriting. 468-487