Handbook of Automated Reasoning

Chapter 9

Rewriting

Nachum Dershowitz

David A. Plaisted

Contents

1  Introduction   537

2  Terminology   541

3  Normal Forms and Validity   544

4  Termination Properties   546

5  Church-Rosser Properties   559

6  Completion   567

7  Relativized Rewriting   574

8  Equational Theorem Proving   581

9  Conditional Rewriting   585

10  Programming   593

Bibliography   597

Index   608

If the work entailed amounts to a virtual rewriting,

the resulting typescript or manuscript is a re-write.

—Eric Partridge, Slang To-day & Yesterday (1933)

1 Introduction

Equations lie at the foundation of mathematics and the sciences. Sometimes one needs to determine if an identity follows logically from axioms; other times, ...