## Term Rewriting SystemsMarc Bezem, J. W. Klop, Roel de Vrijer Term rewriting systems, which developed out of mathematical logic, consist of sequences of discrete steps where one term is replaced with another. Their many applications range from automatic theorem proving systems to computer algebra. This book begins with several examples, followed by a chapter on basic notions that provides a foundation for the rest of the work. First-order and higher-order theories are presented, with much of the latter material appearing for the first time in book form. Subjects treated include orthogonality, termination, lambda calculus and term graph rewriting. There is also a chapter detailing the required mathematical background. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

Introduction | 1 |

Ahstract reduction systems | 7 |

Firstorder term rewriting systems | 24 |

Examples of TRSs and special rewriting formats | 60 |

### Common terms and phrases

A-calculus ahout ahove ahstract reduction system algehraic algorithm amhiguous arhitrary ARSs C(al called chapter CL-term comhinators comhinatory logic common reduct complete TRS computing comumte conflnence Consider the TRS context counterexample Critical Pair Lemma decidahle defined denoted hy diamond property eqnivalence relation equational logic equational specification estahlished example EXERCISE Figure finite function symhol G(al graph rewriting hetween higher-order rewriting hinary Hnet hoth iiil iil Show implication Jan Willem Klop lahelled left-hand side left-linear natural numhers Newman's Lemma normal form notation ohjects ohtained ohvious ouly overlapping redexes possihilities prefix proof Proposition Prove qnestion reduction relation reduction rules reduction seqnence reduction step Reidemeister moves restrictions result rewrite rules riglu-hand side Roel rules pi Section set of equations strongly normalizing suhject suhstitution suhterm symhol F Tahle techniqnes Ter(El term rewriting systems term tree termination Theorem variahles Vrijer wealdy word prohlem