Rewriting Techniques and Applications: 9th International Conference, Rta-98, Tsukuba, Japan, March 30 - April 1, 1998, Proceedings

ISBN-13: 9783540643012 / Angielski / Miękka / 1998 / 346 str.

Tobias Nipkow; T. Nipkow

Opis

A collection of 22 papers covering aspects of rewriting, including: rewriting systems; term rewriting; string rewriting; theorem proving; resolution; normalization; unification; equational logistics; lambda calculus; constraint solving; and functional programming.

Spis treści

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.