Rewrite techniques in theorem proving.- Redundancy criteria for constrained completion.- Bi-rewriting, a term rewriting technique for monotonic order relations.- A case study of completion modulo distributivity and Abelian groups.- A semantic approach to order-sorted rewriting.- Distributing equational theorem proving.- On the correctness of a distributed memory Gröbner basis algorithm.- Improving transformation systems for general E-unification.- Equational and membership constraints for infinite trees.- Regular path expressions in feature logic.- Proving properties of typed lambda terms: Realizability, covers, and sheaves.- Some lambda calculi with categorical sums and products.- Paths, computations and labels in the ?-calculus.- Confluence and superdevelopments.- Relating graph and term rewriting via Böhm models.- Topics in termination.- Total termination of term rewriting.- Simple termination is difficult.- Optimal normalization in orthogonal term rewriting systems.- A graph reduction approach to incremental term rewriting.- Generating tables for bottom-up matching.- On some algorithmic problems for groups and monoids.- Combination techniques and decision problems for disunification.- The negation elimination from syntactic equational formula is decidable.- Encompassment properties and automata with constraints.- Recursively defined tree transductions.- AC complement problems: Satisfiability and negation elimination.- A precedence-based total AC-compatible ordering.- Extension of the associative path ordering to a chain of associative commutative symbols.- Polynomial time termination and constraint satisfaction tests.- Linear interpretations by counting patterns.- Some undecidable termination problems for semi-Thue systems.- Saturation of first-order (constrained) clauses with the Saturate system.- MERILL: An equational reasoning system in standard ML.- Reduce the redex ? ReDuX.- Agg - An implementation of algebraic graph rewriting.- Smaran: A congruence-closure based system for equational computations.- LAMBDALG: Higher order algebraic specification language.- More problems in rewriting.