Contents of the Proceedings of the
8th International Conference on Rewriting Techniques and Applications.
Sitges, Spain, June 2-5, 1997.
Lecture Notes in Computer Science, Vol. 1232, Springer Verlag.
Editor: Hubert Comon.
Invited Talk
- W. McCune,
Well-Behaved Search and the Robbins Problem
(pages 1-7).
Theorem Proving and Rewriting
- C. Lynch,
Goal-Directed Completion Using SOUR Graphs
(pages 8-22).
- D. Kapur,
Shostak's Congruence Closure as Completion
(pages 23-37).
- U. Kühler and C.-P. Wirth,
Conditional Equational Specifications of Data Types with Partial
Operations for Inductive Theorem Proving
(pages 38-52).
String Rewriting
- F. Otto, M. Katsura and Y. Kobayashi,
Cross-Sections for Finitely Presented Monoids with Decidable Word
Problems
(pages 53-67).
- A. Sattler-Klein,
New Undecidablility Results for Finitely Presented Monoids
(pages 68-82).
- F. Otto,
On the Property of Preserving Regularity for String-Rewriting
Systems
(pages 83-97).
Rewriting in Algebraic Theories
- E. Contejean, C. Marché and L. Rabehasaina,
Rewrite Systems for Natural, Integral, and Rational Arithmetic
(pages 98-112).
- L. Bachmair and A. Tiwari,
D-Bases for Polynomial Ideals over Commutative Noetherian Rings
(pages 113-127).
- G. Struth,
On the Word Problem for Free Lattices
(pages 128-141).
Termination
- D. Kapur and G. Sivakumar,
A Total, Ground path Ordering for Proving Termination of AC-Rewrite
Systems
(pages 142-156).
- T. Arts and J. Giesl,
Proving Innermost Normalisation Automatically
(pages 157-171).
- H. Zantema,
Termination of Context-Sensitive Rewriting
(pages 172-186).
Confluence and Termination
- M. Oyamaguchi and Y. Ohta,
A New Parallel Closed Condition for Church-Rossser of Left-Linear
Term Rewriting Systems
(pages 187-201).
- N. Dershowitz,
Innocuous Constructor-Sharing Combinations
(pages 202-216).
- S. M. H. W. Perlo-Freeman and P. Pröhle,
Scott's Conjecture is True, Position Sensitive Weights
(pages 217-227).
Invited Talk
- Y. Lafont,
Two-Dimensional Rewriting
(pages 228-229).
Logic and Rewriting
- D. Bechet, P. de Groote and C. Retoré,
A Complete Axiomatisation for the Inclusion of Series-Parallel
Partial Orders
(pages 230-240).
- J. Marcinkowski,
Undecidability of the First Order Theory of One-Step Right Ground
Rewriting
(pages 241-253).
- S. G. Vorobyov,
The First-Order Theory of One Step Rewriting in Linear Noetherian
Systems is Undecidable
(pages 254-268).
Unification and Constraint Solving
- A. P. Tomás and M. Filgueiras,
Solving Linear Diophantine Equations Using the Geometric Structure
of the Solution Space
(pages 269-283).
- K. U. Schulz,
A Criterion for Intractability of E-unification with Free Function
Symbols and Its Relevance for Combination Algorithms
(pages 284-298).
Higher-Order Rewriting
- R. Statman,
Effective Reduction and Conversion Strategies for Combinators
(pages 299-307).
- V. van Oostrom,
Finite Family Developments
(pages 308-322).
System Descriptions
- C. Ringeissen,
Prototyping Combination of Unification Algorithms with the ELAN
Rule-Based Programming Language
(pages 323-326).
- M. Göbel,
The Invariant Package of MAS
(pages 327-330).
- E. L. Green, L. S. Heath and B. J. Keller,
Opal: A System for Computing Noncommutative Gröbner Bases
(pages 331-334).
- K. Ogata, K. Ohhara and K. Futatsugi,
TRAM: An Abstract Machine for Order-Sorted Conditioned Term
Rewriting Systems
(pages 335-338).