Rewriting Techniques and Applications

Term rewriting and universal algebra in historical perspective.- Characterizations of unification type zero.- Proof normalization for resolution and paramodulation.- Complete sets of reductions modulo associativity, commutativity and identity.- Completion-time optimization of rewrite-time goal solving.- Computing ground reducibility and inductively complete positions.- Inductive proofs by specification transformations.- Narrowing and unification in functional programming -An evaluation mechanism for absolute set abstraction.- Simulation of Turing machines by a left-linear rewrite rule.- Higher-order unification with dependent function types.- An overview of LP, the Larch Prover.- Graph grammars, a new paradigm for implementing visual languages.- Termination proofs and the length of derivations.- Abstract rewriting with concrete operators.- On how to move mountains 'associatively and commutatively'.- Generalized Gröbner bases: Theory and applications. A condensation.- A local termination property for term rewriting systems.- An equational logic sampler.- Modular aspects of properties of term rewriting systems related to normal forms.- Priority rewriting: Semantics, confluence, and conditionals.- Negation with logical variables in conditional rewriting.- Algebraic semantics and complexity of term rewriting systems.- Optimization by non-deterministic, lazy rewriting.- Combining matching algorithms: The regular case.- Restrictions of congruences generated by finite canonical string-rewriting systems.- Embedding with patterns and associated recursive path ordering.- Rewriting techniques for program synthesis.- Transforming strongly sequential rewrite systems with constructors for efficient parallel execution.- Efficient ground completion.- Extensions and comparison of simplification orderings.- Classes of equational programs that compile into efficient machine code.- Fair termination is decidable for ground systems.- Termination for the direct sum of left-linear term