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.2015.269
URN: urn:nbn:de:0030-drops-52024
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5202/
Go to the corresponding LIPIcs Volume Portal

Nagele, Julian ; Zankl, Harald

Certified Rule Labeling

pdf-format:
22.pdf (0.6 MB)

Abstract

The rule labeling heuristic aims to establish confluence of (left-)linear term rewrite systems via decreasing diagrams. We present a formalization of a confluence criterion based on the interplay of relative termination and the rule labeling in the theorem prover Isabelle. Moreover, we report on the integration of this result into the certifier CeTA, facilitating the checking of confluence certificates based on decreasing diagrams for the first time. The power of the method is illustrated by an experimental evaluation on a (standard) collection of confluence problems.

BibTeX - Entry

@InProceedings{nagele_et_al:LIPIcs:2015:5202,
  author =	{Julian Nagele and Harald Zankl},
  title =	{{Certified Rule Labeling}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{269--284},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Maribel Fern{\'a}ndez},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5202},
  URN =		{urn:nbn:de:0030-drops-52024},
  doi =		{10.4230/LIPIcs.RTA.2015.269},
  annote =	{Keywords: term rewriting, confluence, decreasing diagrams, certification}
}

Keywords: term rewriting, confluence, decreasing diagrams, certification
Collection: 26th International Conference on Rewriting Techniques and Applications (RTA 2015)
Issue Date: 2015
Date of publication: 18.06.2015

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