License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2010.7
URN: urn:nbn:de:0030-drops-26418
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2641/
Go to the corresponding LIPIcs Volume Portal

Aoto, Takahito

Automated Confluence Proof by Decreasing Diagrams based on Rule-Labelling

pdf-format:
10002.AotoTakahito.2641.pdf (0.1 MB)

Abstract

Decreasing diagrams technique (van Oostrom, 1994) is a technique that
can be widely applied to prove confluence of rewrite systems. To
directly apply the decreasing diagrams technique to prove confluence
of rewrite systems, rule-labelling heuristic has been proposed by van
Oostrom (2008). We show how constraints for ensuring confluence of
term rewriting systems constructed based on the rule-labelling
heuristic are encoded as linear arithmetic constraints suitable for
solving the satisfiability of them by external SMT solvers. We point
out an additional constraint omitted in (van Oostrom, 2008) that is
needed to guarantee the soundness of confluence proofs based on the
rule-labelling heuristic extended to deal with non-right-linear rules.
We also present several extensions of the rule-labelling heuristic by
which the applicability of the technique is enlarged.

BibTeX - Entry

@InProceedings{aoto:LIPIcs:2010:2641,
  author =	{Takahito Aoto},
  title =	{{Automated Confluence Proof by Decreasing Diagrams based on Rule-Labelling}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{7--16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Christopher Lynch},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2010/2641},
  URN =		{urn:nbn:de:0030-drops-26418},
  doi =		{10.4230/LIPIcs.RTA.2010.7},
  annote =	{Keywords: Confluence, Decreasing Diagrams, Automation, Term Rewriting Systems}
}

Keywords: Confluence, Decreasing Diagrams, Automation, Term Rewriting Systems
Collection: Proceedings of the 21st International Conference on Rewriting Techniques and Applications
Issue Date: 2010
Date of publication: 06.07.2010

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