Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Nagele, Julian; Felgenhauer, Bertram; Middeldorp, Aart http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-52010
URL:

; ;

Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules

pdf-format:


Abstract

We describe how to utilize redundant rewrite rules, i.e., rules that can be simulated by other rules, when (dis)proving confluence of term rewrite systems. We demonstrate how automatic confluence provers benefit from the addition as well as the removal of redundant rules. Due to their simplicity, our transformations were easy to formalize in a proof assistant and are thus amenable to certification. Experimental results show the surprising gain in power.

BibTeX - Entry

@InProceedings{nagele_et_al:LIPIcs:2015:5201,
  author =	{Julian Nagele and Bertram Felgenhauer and Aart Middeldorp},
  title =	{{Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{257--268},
  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/5201},
  URN =		{urn:nbn:de:0030-drops-52010},
  doi =		{10.4230/LIPIcs.RTA.2015.257},
  annote =	{Keywords: term rewriting, confluence, automation, transformation}
}

Keywords: term rewriting, confluence, automation, transformation
Seminar: 26th International Conference on Rewriting Techniques and Applications (RTA 2015)
Issue date: 2015
Date of publication: 2015


DROPS-Home | Fulltext Search | Imprint Published by LZI