3. RTA 1989: Chapel Hill, North Carolina, USA

Invited Lecture

• Garrett Birkhoff:
  Term Rewriting and Universal Algebra in Historical Perspective (Abstract of Invited Lecture). 1
  

Regular Papers

• Franz Baader:
  Characterization of Unification Type Zero. 2-14
  
• Leo Bachmair:
  Proof Normalization for Resolution and Paramodulation. 15-28
  
• Timothy B. Baird, Gerald E. Peterson, Ralph W. Wilkerson:
  Complete Sets of Reductions Modulo Associativity, Commutativity and Identity. 29-44
  
• Hubert Bertling, Harald Ganzinger:
  Completion-Time Optimization of Rewrite-Time Goal Solving. 45-58
  
• Reinhard Bündgen, Wolfgang Küchlin:
  Computing Ground Reducability and Inductively Complete Positions. 59-75
  
• Hubert Comon:
  Inductive Proofs by Specification Transformation. 76-91
  
• John Darlington, Yike Guo:
  Narrowing and Unification in Functional Programming - An Evaluation Mechanism for Absolute Set Abstraction. 92-108
  
• Max Dauchet:
  Simulation of Turning Machines by a Left-Linear Rewrite Rule. 109-120
  
• Conal Elliott:
  Higher-order Unification with Dependent Function Types. 121-136
  
• Stephen J. Garland, John V. Guttag:
  An Overview of LP, The Larch Power. 137-151
  
• Herbert Göttler:
  Graph Grammars, A New Paradigma for Implementing Visual Languages. 152-166
  
• Dieter Hofbauer, Clemens Lautemann:
  Termination Proofs and the Length of Derivations (Preliminary Version). 167-177
  
• Stéphane Kaplan, Christine Choppy:
  Abstract Rewriting with Concrete Operations. 178-186
  
• Mike Lai:
  On How To Move Mountains 'Associatively and Commutatively'. 187-202
  
• Dallas Lankford:
  Generalized Gröbner Bases: Theory and Applications. A Condensation. 203-221
  
• Dana May Latch, Ron Sigal:
  A Local Termination Property for Term Rewriting Systems. 222-233
  
• George F. McNulty:
  An Equational Logic Sampler. 234-262
  
• Aart Middeldorp:
  Modular Aspects of Properties of Term Rewriting Systems Related to Normal Forms. 263-277
  
• Chilukuri K. Mohan:
  Priority Rewriting: Semantics, Confluence, and Conditional. 278-291
  
• Chilukuri K. Mohan, Mandayam K. Srivas:
  Negation with Logical Variables in Conditional Rewriting. 292-310
  
• Tohru Naoi, Yasuyoshi Inagaki:
  Algebraic Semantics and Complexity of Term Rewriting Systems. 311-325
  
• Sanjai Narain:
  Optimization by Non-Deterministic, Lazy Rewriting. 326-342
  
• Tobias Nipkow:
  Combining Matching Algorithms: The Rectangular Case. 343-358
  
• Friedrich Otto:
  Restrictions of Congruence Generated by Finite Canonical String-Rewriting Systems. 359-370
  
• Laurence Puel:
  Embedding with Patterns and Associated Recursive Path Ordering. 371-387
  
• Uday S. Reddy:
  Rewriting Techniques for Program Synthesis. 388-403
  
• R. C. Sekar, Shaunak Pawagi, I. V. Ramakrishnan:
  Transforming Strongly Sequential Rewrite Systems with Constructors for Efficient parallel Execution. 404-418
  
• Wayne Snyder:
  Efficient Ground Completion: An O(n log n) Algorithm for Generating Reduced Sets of Ground Rewrite Rules Equivalent to a Set of Ground Equations E. 419-433
• Joachim Steinbach:
  Extensions and Comparison of Simplification Orderings. 434-448
  
• Robert Strandh:
  Classes of Equational Programs that Compile into Efficient Machine Code. 449-461
  
• Sophie Tison:
  Fair Termination is Decidable for Ground Systems. 462-476
  
• Yoshihito Toyama, Jan Willem Klop, Hendrik Pieter Barendregt:
  Termination for the Direct Sum of left-Linear Term Rewriting Systems -Preliminary Draft-. 477-491
  
• Sergei G. Vorobyov:
  Conditional Rewrite Rule Systems with Built-In Arithmetic and Induction. 492-512
  
• Hantao Zhang, Deepak Kapur:
  Consider Only General Superpositions in Completion Procedures. 513-527
  

System Descriptions

• Habib Abdulrab, Jean-Pierre Pécuchet:
  Solving Systems of Linear Diophantine Equations and Word Equations. 530-532
  
• Siva Anantharaman, Jieh Hsiang, Jalel Mzali:
  SbReve2: A Term Rewriting Laboratory with (AC-) Unfailing Completion. 533-537
  
• Jürgen Avenhaus, Jörg Denzinger, Jürgen Müller:
  THEOPOGLES - An efficient Theorem Prover based on Rewrite-Techniques. 538-541
  
• Jürgen Avenhaus, Klaus Madlener, Joachim Steinbach:
  COMTES - An Experimental Environment for the Completion of Term Rewriting Systems. 542-546
  
• Michel Bidoit, Francis Capy, Christine Choppy:
  ASSPEGIQUE: An Integrated Specification Environment. 547
  
• Maria Paola Bonacina, Giancarlo Sanna:
  KBlab: An Equational Theorem Prover for the Macintosh. 548-550
  
• Jim Christian:
  Fast Knuth-Bendix Completion: Summary. 551-555
  
• Max Dauchet, Aline Deruyver:
  Compilation of Ground Term Rewriting Systems and Applications. 556-558
  
• Deepak Kapur, Hantao Zhang:
  An Overview of Rewrite Rule Laboratory (RRL). 559-563
  
• Hessam Khoshnevisan, K. M. Sephton:
  InvX: An Automatic Function Inverter. 564-568
  
• Naomi Lindenstrauss:
  A Parallel Implementation of Rewriting and Narrowing. 569-573
  
• John Pedersen:
  Morphocompletion for One-Relation Monoids. 574-578