8. RTA 1997: Sitges, Spain

Invited Talk

• William McCune:
  Well-Behaved Search and the Robbins Problem. 1-7
  

Session 1: Theorem Proving and Rewriting

• Christopher Lynch:
  Goal-Directed Completion Using SOUR Graphs. 8-22
  
• Deepak Kapur:
  Shostak's Congruence Closure as Completion. 23-37
  
• Ulrich Kühler, Claus-Peter Wirth:
  Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving. 38-52
  

Session 2: String Rewriting

• Friedrich Otto, Masashi Katsura, Yuji Kobayashi:
  Cross-Sections for Finitely Presented Monoids with Decidable Word Problems. 53-67
  
• Andrea Sattler-Klein:
  New Undecidablility Results for Finitely Presented Monoids. 68-82
  
• Friedrich Otto:
  On the Property of Preserving Regularity for String-Rewriting Systems. 83-97
  

Session 3: Rewriting in Algebraic Theories

• Evelyne Contejean, Claude Marché, Landy Rabehasaina:
  Rewrite Systems for Natural, Integral, and Rational Arithmetic. 98-112
  
• Leo Bachmair, Ashish Tiwari:
  D-Bases for Polynomial Ideals over Commutative Noetherian Rings. 113-127
  
• Georg Struth:
  On the Word Problem for Free Lattices. 128-141
  

Session 4: Termination

• Deepak Kapur, G. Sivakumar:
  A Total, Ground path Ordering for Proving Termination of AC-Rewrite Systems. 142-156
  
• Thomas Arts, Jürgen Giesl:
  Proving Innermost Normalisation Automatically. 157-171
  
• Hans Zantema:
  Termination of Context-Sensitive Rewriting. 172-186
  

Session 5: Confluence and Termination

• Michio Oyamaguchi, Yoshikatsu Ohta:
  A New Parallel Closed Condition for Church-Rossser of Left-Linear Term Rewriting Systems. 187-201
  
• Nachum Dershowitz:
  Innocuous Constructor-Sharing Combinations. 202-216
  
• Samuel M. H. W. Perlo-Freeman, Péter Pröhle:
  Scott's Conjecture is True, Position Sensitive Weights. 217-227
  

Invited Talk

• Yves Lafont:
  Two-Dimensional Rewriting. 228-229
  

Session 6: Logic and Rewriting

• Denis Béchet, Philippe de Groote, Christian Retoré:
  A Complete Axiomatisation for the Inclusion of Series-Parallel Partial Orders. 230-240
  
• Jerzy Marcinkowski:
  Undecidability of the First Order Theory of One-Step Right Ground Rewriting. 241-253
  
• Sergei G. Vorobyov:
  The First-Order Theory of One Step Rewriting in Linear Noetherian Systems is Undecidable. 254-268
  

Session 7: Unification and Constraint Solving

• Ana Paula Tomás, Miguel Filgueiras:
  Solving Linear Diophantine Equations Using the Geometric Structure of the Solution Space. 269-283
  
• Klaus U. Schulz:
  A Criterion for Intractability of E-unification with Free Function Symbols and Its Relevance for Combination Algorithms. 284-298
  

Session 8: Higher-Order Rewriting

• Richard Statman:
  Effective Reduction and Conversion Strategies for Combinators. 299-307
  
• Vincent van Oostrom:
  Finite Family Developments. 308-322
  

System Descriptions

• Christophe Ringeissen:
  Prototyping Combination of Unification Algorithms with the ELAN Rule-Based Programming Language. 323-326
  
• Manfred Göbel:
  The Invariant Package of MAS. 327-330
  
• Edward L. Green, Lenwood S. Heath, Benjamin J. Keller:
  Opal: A System for Computing Noncommutative Gröbner Bases. 331-334
  
• Kazuhiro Ogata, Koichi Ohhara, Kokichi Futatsugi:
  TRAM: An Abstract Machine for Order-Sorted Conditioned Term Rewriting Systems. 335-338
  

Last update Wed Feb 15 05:16:21 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page