Rewriting Techniques and Applications: Dijon, France, May 20–22, 1985

Bruno Buchberger (auth.), Jean-Pierre Jouannaud (eds.)9783540159766, 3540159762

The theory and practice of term rewriting is now well-established and the focus of growing interest in the world of computer science. This book brings together a collection of original research contributions and surveys of existing knowledge. Some of the most significant developments in term rewriting theory are reviewed, as well as a history of the most important discovery in the field, namely the notion of a critical pair and its natural consequence, the completion algorithm. Many of the new ideas developed have important applications in other fields of theoretical computing. Therefore, this book should be of interest to researchers from areas such as logic programming, computer algebra, and functional programming.

---

Table of contents :
Basic features and development of the critical-pair/completion procedure….Pages 1-45
Contextual rewriting….Pages 46-62
Thue systems as rewriting systems….Pages 63-94
Deciding algebraic properties of monoids presented by finite church-rosser Thue systems….Pages 95-106
Two applications of equational theories to database theory….Pages 107-123
An experiment in partial evaluation: The generation of a compiler generator….Pages 124-140
NARROWER: a new algorithm for unification and its application to Logic Programming….Pages 141-157
Solving type equations by graph rewriting….Pages 158-179
Termination….Pages 180-224
Path of subterms ordering and recursive decomposition ordering revisited….Pages 225-240
Associative path orderings….Pages 241-254
A procedure for automatically proving the termination of a set of rewrite rules….Pages 255-270
Petrireve: Proving Petri net properties with rewriting systems….Pages 271-286
Fairness in term rewriting systems….Pages 287-300
Two results in term rewriting theorem proving….Pages 301-324
Handling function definitions through innermost superposition and rewriting….Pages 325-344
An ideal-theoretic approach to word problems and unification problems over finitely presented commutative algebras….Pages 345-364
Combining unification algorithms for confined regular equational theories….Pages 365-380
An algebraic approach to unification under associativity and commutativity….Pages 381-397
Unification problems with one-sided distributivity….Pages 398-406
Fast many-to-one matching algorithms….Pages 407-416
Complexity of matching problems….Pages 417-429
The set of unifiers in typed λ-calculus as regular expression….Pages 430-440
Equational systems for category theory and intuitionistic logic….Pages 441-441