|
Abstract
Rewriting
Title: |
Abstract Rewriting |
Author: |
Christian Sternagel and René Thiemann |
Submission date: |
2010-06-14 |
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.
|
Change history: |
[2010-09-17]: Added theories defining several (ordered)
semirings related to strong normalization and giving some standard
instances.
[2013-10-16]: Generalized delta-orders from rationals to Archimedean fields.
|
BibTeX: |
@article{Abstract-Rewriting-AFP,
author = {Christian Sternagel and René Thiemann},
title = {Abstract Rewriting},
journal = {Archive of Formal Proofs},
month = jun,
year = 2010,
note = {\url{http://isa-afp.org/entries/Abstract-Rewriting.shtml},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
GNU Lesser General Public License (LGPL) |
Depends on: |
Regular-Sets |
Used by: |
Algebraic_Numbers, Decreasing-Diagrams, Decreasing-Diagrams-II, Groebner_Bases, Jordan_Normal_Form, Matrix, Polynomials, Rewriting_Z, Well_Quasi_Orders |
Status: [ok] |
This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|