Abstract Rewriting

Christian Sternagel 📧 and René Thiemann 🌐

June 14, 2010

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

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.

License

GNU Lesser General Public License (LGPL)

History

October 16, 2013
Generalized delta-orders from rationals to Archimedean fields.
September 17, 2010
Added theories defining several (ordered) semirings related to strong normalization and giving some standard instances.

Topics

Session Abstract-Rewriting