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.FSCD.2016.29
URN: urn:nbn:de:0030-drops-59996
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/5999/
Go to the corresponding LIPIcs Volume Portal

Sternagel, Christian ; Sternagel, Thomas

Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion

pdf-format:
LIPIcs-FSCD-2016-29.pdf (0.6 MB)

Abstract

Suzuki et al. showed that properly oriented, right-stable, orthogonal, and oriented conditional term rewrite systems with extra variables in right-hand sides are confluent. We present our Isabelle/HOL formalization of this result, including two generalizations. On the one hand, we relax proper orientedness and orthogonality to extended proper orientedness and almost orthogonality modulo infeasibility, as suggested by Suzuki et al. On the other hand, we further loosen the requirements of the latter, enabling more powerful methods for proving infeasibility of conditional critical pairs. Furthermore, we formalized a construction by Jacquemard that employs exact tree automata completion for non-reachability analysis and apply it to certify infeasibility of conditional critical pairs. Combining these two results and extending the conditional confluence checker ConCon accordingly, we are able to automatically prove and certify confluence of an important class of conditional term rewrite systems.

BibTeX - Entry

@InProceedings{sternagel_et_al:LIPIcs:2016:5999,
  author =	{Christian Sternagel and Thomas Sternagel},
  title =	{{Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{29:1--29:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Delia Kesner and Brigitte Pientka},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/5999},
  URN =		{urn:nbn:de:0030-drops-59996},
  doi =		{10.4230/LIPIcs.FSCD.2016.29},
  annote =	{Keywords:  certification, conditional term rewriting, confluence, infeasible critical pairs, non-reachability}
}

Keywords: certification, conditional term rewriting, confluence, infeasible critical pairs, non-reachability
Collection: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Issue Date: 2016
Date of publication: 17.06.2016

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