License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2013.352
URN: urn:nbn:de:0030-drops-40723
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4072/
Go to the corresponding LIPIcs Volume Portal

Zankl, Harald

Confluence by Decreasing Diagrams – Formalized

pdf-format:
25.pdf (0.5 MB)

Abstract

This paper presents a formalization of decreasing diagrams in the theorem prover Isabelle. It discusses mechanical proofs showing that any locally decreasing abstract rewrite system is confluent. The valley and the conversion version of decreasing diagrams are considered.

BibTeX - Entry

@InProceedings{zankl:LIPIcs:2013:4072,
  author =	{Harald Zankl},
  title =	{{Confluence by Decreasing Diagrams – Formalized}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{352--367},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{Femke van Raamsdonk},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4072},
  URN =		{urn:nbn:de:0030-drops-40723},
  doi =		{10.4230/LIPIcs.RTA.2013.352},
  annote =	{Keywords: term rewriting, confluence, decreasing diagrams, formalization}
}

Keywords: term rewriting, confluence, decreasing diagrams, formalization
Collection: 24th International Conference on Rewriting Techniques and Applications (RTA 2013)
Issue Date: 2013
Date of publication: 24.06.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI