| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Decreasing Diagrams
| Title: | Decreasing Diagrams |
| Author: | Harald Zankl |
| Submission date: | 2013-11-01 |
| Abstract: | This theory contains a formalization of decreasing diagrams showing that any locally decreasing abstract rewrite system is confluent. We consider the valley (van Oostrom, TCS 1994) and the conversion version (van Oostrom, RTA 2008) and closely follow the original proofs. As an application we prove Newman's lemma. |
| BibTeX: |
@article{Decreasing-Diagrams-AFP,
author = {Harald Zankl},
title = {Decreasing Diagrams},
journal = {Archive of Formal Proofs},
month = nov,
year = 2013,
note = {\url{http://isa-afp.org/entries/Decreasing-Diagrams.shtml},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | GNU Lesser General Public License (LGPL) |
| Depends on: | Abstract-Rewriting |
| Status: [skipped] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|