| Home |
| About |
| Submission Guidelines |
| Updating entries |
| Search |
| Index |
| Download |
project summary
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. |
| 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://afp.sf.net/entries/Abstract-Rewriting},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | GNU Lesser General Public License (LGPL) |
| Status: [ok] | This is the development version, revision 4b34a59339a6, of this entry, generated for Isabelle revision 895d12fc0dd7. The development version might change over time and is only permanently archived at Isabelle release points. It is provided as a preview of the next upcoming release. Please refer to release versions only in citations. If the status shows [FAIL], the links below will point to the last working version if any. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|