4. RTA 1991: Como, Italy

• Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, Fer-Jan de Vries:
  Transfinite Reductions in Orthogonal Term Rewriting Systems (Extended Abstract). 1-12
  
• William M. Farmer, Ronald J. Watro:
  Redex Capturing in Term Graph Rewriting (Concise Version). 13-24
  
• David A. Wolfram:
  Rewriting, and Equational Unification: the Higher-Order Cases. 25-36
  
• Daniel J. Dougherty:
  Adding Algebraic Rewriting to the Untyped Lambda Calculus (Extended Abstract). 37-48
  
• Frank Drewes, Clemens Lautemann:
  Incremental Termination Proofs and the Length of Derivations. 49-61
  
• Dieter Hofbauer:
  Time Bounded Rewrite Systems and Termination Proofs by Generalized Embedding. 62-73
  
• Stefan Krischer, Alexander Bockmayr:
  Detecting Redundant Narrowing Derivations by the LSE-SL Reducability Test. 74-85
  
• Franz Baader:
  Unification, Weak Unification, Upper Bound, Lower Bound, and Generalization Problems. 86-97
  
• Eric Domenjoud:
  AC Unification Through Order-Sorted AC1 Unification. 98-111
  
• Jacques Chabin, Pierre Réty:
  Narrowing Directed by a Graph of Terms. 112-123
  
• Franz Baader, Werner Nutt:
  Adding Homomorphisms to Commutative/Monoidal Theories or How Algebra Can Help in Equational Unification. 124-135
  
• Francis Klay:
  Undecidable Properties of Syntactic Theories. 136-149
  
• Wayne Snyder, Christopher Lynch:
  Goal Directed Strategies for Paramodulation. 150-161
  
• Loic Pottier:
  Minimal Solutions of Linear Diophantine Systems: Bounds and Algorithms. 162-173
  
• Hélène Kirchner:
  Proofs in Parameterized Specification. 174-187
  
• Aart Middeldorp, Yoshihito Toyama:
  Completeness of Combinations of Constructor Systems. 188-199
  
• Tobias Nipkow, Zhenyu Qian:
  Modular Higher-Order E-Unification. 200-214
  
• Pierre-Louis Curien, Giorgio Ghelli:
  On Confluence for Weakly Normalizing Systems. 215-225
  
• Françoise Bellegarde:
  Program Transformation and Rewriting. 226-239
  
• Dave Cohen, Phil Watson:
  An Efficient Representation of Arithmetic for Term Rewriting. 240-251
  
• Sieger van Denneheuvel, Karen L. Kwast, Gerard R. Renardel de Lavalette, Edith Spaan:
  Query Optimization Using Rewrite Rules. 252-263
  
• Rolf Socher-Ambrosius:
  Boolean Algebra Admits No Convergent Term Rewriting System. 264-274
  
• Kai Salomaa:
  Decidability of Confluence and Termination of Monadic Term Rewriting Systems. 275-286
  
• Jean-Luc Coquidé, Max Dauchet, Rémi Gilleron, Sándor Vágvölgyi:
  Bottom-Up Tree Pushdown Automata and Rewrite Systems. 287-298
  
• Gregory Kucherov:
  On Relationship Between Term Rewriting Systems and Regular Tree Languages. 299-311
  
• Franz-Josef Brandenburg:
  The Equivalence of Boundary and Confluent Graph Grammars on Graph Languages of Bounded Degree. 312-322
  
• Albert Gräf:
  Left-to-Right Tree Pattern Matching. 323-334
  
• R. Ramesh, I. V. Ramakrishnan:
  Incremental Techniques for Efficient Normalization of Nonlinear Rewrite Systems. 335-347
  
• Maria Paola Bonacina, Jieh Hsiang:
  On Fairness of Completion-Based Theorem Proving Strategies. 348-360
  
• Jürgen Avenhaus:
  Proving Equational and Inductive Theorems by Completion and Embedding Techniques. 361-373
  
• Andrea Sattler-Klein:
  Divergence Phenomena during Completion. 374-385
  
• Reinhard Bündgen:
  Simulation Buchberger's Algorithm by Knuth-Bendix Completion. 386-397
  
• Miki Hermann:
  On Proving Properties of Completion Strategies. 398-410
  
• Claude Marché:
  On Ground AC-Completion. 411-422
  
• Paliath Narendran, Michaël Rusinowitch:
  Any Gound Associative-Commutative Theory Has a Finite Canonical System. 423-434
  
• Ulrich Fraus:
  A Narrowing-Based Theorem Prover. 435-436
  
• Michel Billaud:
  ANIGRAF: An Interactive System for the Animation of Graph Rewriting Systems with Priorities. 437-438
  
• Aline Deruyver:
  EMMY: A Refutational Theorem Prover for First-Order Logic with Equation. 439-441
  
• Raj Agarwal, David R. Musser, Deepak Kapur, Xumin Nie:
  The Tecton Proof System. 442-444
  
• Nachum Dershowitz, Jean-Pierre Jouannaud, Jan Willem Klop:
  Open Problems in Rewriting. 445-456