cl-banner

Decreasing Diagrams

Harald Zankl

Archive of Formal Proofs, 2013.

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.

 

   AFP entry  

BibTeX 

@incollection{13HZ-AFP,
author = "Harald Zankl",
title = "Decreasing Diagrams",
booktitle = "The Archive of Formal Proofs",
editor = "Gerwin Klein and Tobias Nipkow and Lawrence Paulson",
publisher = "\url{http://afp.sf.net/entries/Decreasing-Diagrams.shtml}",
month = nov,
year = 2013,
note = {Formal proof development},
ISSN = {2150-914x}
}
Nach oben scrollen