Term rewriting

This chapter 9 of the book introduces term rewriting and some of its applications from different points of view. In the first part it presents the basic notions and results and in the second part the focus is on applications in the areas of prototyping algebraic specifications and theorem proving. The paper gives a good overview on what has been developed in this direction over the last thirty years. In Section 9.1 the abstract notion of a rewriting relation is introduced, including the basic notions of termination and confluence and techniques to prove these properties. In Section 9.2 this is specialized to term rewriting. In Section 9.3 the rewriting logic is introduced and it is demonstrated how to use it to describe concurrent computations and proof systems. The second part of the paper starts with Section 9.4 which is devoted to first-order theorem proving. Here, the completion procedure of Knuth and Bendix is the starting point for the development of now highly efficient algorithms for first-order theorem proving, solving equations modulo a theory and deduction with constraints. Section 9.5 follows with modeling order sorted specifications by order sorted rewrite systems. Finally, in Section 9.6 rewrite techniques are applied to find proofs for theorems in the initial algebra defined by an equational specification. For the entire collection see [Zbl 0973.68002].

Recommendations

Cited in

(25)

Describes a project that uses

Uses Software

ELAN

This page was built for publication: Term rewriting

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4702599)