Term rewriting and all that. (English) Zbl 0948.68098

Cambridge: Cambridge University Press. xii, 301 p. (1999).
The current book is devoted to the theory and applications of term rewriting. It contains the basic material of this field, in particular abstract reduction systems, termination problems, confluence completion, and combination problems. But also closely related topics are expounded as universal algebra, unification theory, Gröbner bases and Buchberger’s algorithm. Relevant results that are dissiminated over many conference proceedings and journal articles are collected together and presented in a unified notation and terminology, detailed proofs of the theorems are given, and each chapter closes with bibliographic notes containing historical remarks and a brief guide to the literature. The book contains many examples and over 170 exercises.
The most important algorithms are presented both in a descriptive, informal manner but also as programs in the functional language Standard ML. In addition, the appendix contains a transparent and easy introduction to ML. The most important algorithms like unification and congruence closure are studied in detail and efficient Pascal programs are developed.
In summary, the book is welcomed to students and to researchers working on the field of theoretical computer science. It is a well-balanced textbook on these topics presenting the subject in a unified and systematic manner.
Reviewer: H.Herre (Leipzig)


68Q42 Grammars and rewriting systems
03B35 Mechanization of proofs and logical operations
08A70 Applications of universal algebra in computer science
68-02 Research exposition (monographs, survey articles) pertaining to computer science


term rewriting


Full Text: DOI