Rewriting Techniques and Applications

Origin tracking in term rewriting.- Simultaneous critical pairs and Church-Rosser property.- Church-Rosser theorems for abstract reduction modulo an equivalence relation.- Automatic monoids versus monoids with finite convergent presentations.- Decidable and undecidable second-order unification problems.- On the exponent of periodicity of minimal solutions of context equations.- Unification in extensions of shallow equational theories.- Unification and matching in process algebras.- E-unification for subsystems of S4.- Solving disequations modulo some class of rewrite systems.- About proofs by consistency.- Normalization of S-terms is decidable.- Decidable approximations of sets of descendants and sets of normal forms.- Algorithms and reductions for rewriting problems.- The decidability of simultaneous rigid E-unification with one variable.- Ordering constraints over feature trees expressed in second-order monadic logic.- Co-definite set constraints.- Modularity of termination using dependency pairs.- Termination of associative-commutative rewriting by dependency pairs.- Termination transformation by tree lifting ordering.- Towards automated termination proofs through “freezing”.- Higher-order rewriting and partial evaluation.- SN combinators and partial combinatory algebras.- Coupling saturation-based provers by exchanging positive/negative information.- An on-line problem database.