Decreasing Diagrams (Q7361048)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Decreasing-Diagrams
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Decreasing Diagrams |
AFP entry Decreasing-Diagrams |
Statements
1 November 2013
0 references
Harald Zankl
0 references
Decreasing Diagrams (English)
0 references
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.
0 references