Abstract is missing.
- Well-Behaved Search and the Robbins ProblemWilliam McCune. 1-7
- Goal-Directed Completion Using SOUR GraphsChristopher Lynch. 8-22
- Shostak s Congruence Closure as CompletionDeepak Kapur. 23-37
- Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem ProvingUlrich Kühler, Claus-Peter Wirth. 38-52
- Cross-Sections for Finitely Presented Monoids with Decidable Word ProblemsFriedrich Otto, Masashi Katsura, Yuji Kobayashi. 53-67
- New Undecidablility Results for Finitely Presented MonoidsAndrea Sattler-Klein. 68-82
- On the Property of Preserving Regularity for String-Rewriting SystemsFriedrich Otto. 83-97
- Rewrite Systems for Natural, Integral, and Rational ArithmeticEvelyne Contejean, Claude Marché, Landy Rabehasaina. 98-112
- D-Bases for Polynomial Ideals over Commutative Noetherian RingsLeo Bachmair, Ashish Tiwari. 113-127
- On the Word Problem for Free LatticesGeorg Struth. 128-141
- A Total, Ground path Ordering for Proving Termination of AC-Rewrite SystemsDeepak Kapur, G. Sivakumar. 142-156
- Proving Innermost Normalisation AutomaticallyThomas Arts, Jürgen Giesl. 157-171
- Termination of Context-Sensitive RewritingHans Zantema. 172-186
- A New Parallel Closed Condition for Church-Rossser of Left-Linear Term Rewriting SystemsMichio Oyamaguchi, Yoshikatsu Ohta. 187-201
- Innocuous Constructor-Sharing CombinationsNachum Dershowitz. 202-216
- Scott s Conjecture is True, Position Sensitive WeightsSamuel M. H. W. Perlo-Freeman, Péter Pröhle. 217-227
- Two-Dimensional RewritingYves Lafont. 228-229
- A Complete Axiomatisation for the Inclusion of Series-Parallel Partial OrdersDenis Béchet, Philippe de Groote, Christian Retoré. 230-240
- Undecidability of the First Order Theory of One-Step Right Ground RewritingJerzy Marcinkowski. 241-253
- The First-Order Theory of One Step Rewriting in Linear Noetherian Systems is UndecidableSergei G. Vorobyov. 254-268
- Solving Linear Diophantine Equations Using the Geometric Structure of the Solution SpaceAna Paula Tomás, Miguel Filgueiras. 269-283
- A Criterion for Intractability of E-unification with Free Function Symbols and Its Relevance for Combination AlgorithmsKlaus U. Schulz. 284-298
- Effective Reduction and Conversion Strategies for CombinatorsRichard Statman. 299-307
- Finite Family DevelopmentsVincent van Oostrom. 308-322
- Prototyping Combination of Unification Algorithms with the ELAN Rule-Based Programming LanguageChristophe Ringeissen. 323-326
- The Invariant Package of MASManfred Göbel. 327-330
- Opal: A System for Computing Noncommutative Gröbner BasesEdward L. Green, Lenwood S. Heath, Benjamin J. Keller. 331-334
- TRAM: An Abstract Machine for Order-Sorted Conditioned Term Rewriting SystemsKazuhiro Ogata, Koichi Ohhara, Kokichi Futatsugi. 335-338