Abstract Rewriting

Christian Sternagel and René Thiemann

The Archive of Formal Proofs, 2010.


We present an Isabelle formalization of abstract rewriting (see, e.g., the book by Baader and Nipkow). First, we define standard relations like joinability, meetability, conversion, etc. Then, we formalize important properties of abstract rewrite systems, e.g., confluence and strong normalization. Our main concern is on strong normalization, since this formalization is the basis of CeTA (which is mainly about strong normalization of term rewrite systems). Hence lemmas involving strong normalization constitute by far the biggest part of this theory. One of those is Newman’s lemma.


   AFP entry


author = "Christian Sternagel and Ren{\'e} Thiemann",
title = "{A}bstract {R}ewriting}",
booktitle = "The Archive of Formal Proofs",
editor = "Gerwin Klein and Tobias Nipkow and Lawrence Paulson",
publisher = "\url{}",
year = 2010,
month = Jun,
note = "Formal proof development"
ISSN = "2150-914x",
Nach oben scrollen