Lecture Notes in Computer Science

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 Grobner 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 rewriting systems.- Conditional rewrite rule systems with built-in arithmetic and induction.- Consider only general superpositions in completion procedures.- Solving systems of linear diophantine equations and word equations.- SbReve2: A term rewriting laboratory with (AC)-unfailing completion.- THEOPOGLES - An efficient theorem prover based on rewrite-techniques.- Comtes - An experimental environment for the completion of term rewriting systems.- Asspegique: An integrated specification environment.- KBlab: An equational theorem prover for the Macintosh.- Fast Knuth-Bendix completion: Summary.- Compilation of ground term rewriting systems and applications (DEMO).- An overview of Rewrite Rule Laboratory (RRL).- InvX: An automatic function inverter.- A parallel implementation of rewriting and narrowing.- Morphocompletion for one-relation monoids.