Abstract
Franz Baader and Tobias Nipkow’s book is a standard introduction to first-order term rewriting systems and their metatheory. It develops the basic theory of abstract reduction systems, including confluence, normal forms, and termination, and then studies completion, equational reasoning, and connections with automated deduction.
Outline
Core topics
- abstract reduction systems
- term rewriting systems
- Confluence and Church-Rosser properties
- termination and normal forms
- Completion procedures and equational reasoning