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.2017.7
URN: urn:nbn:de:0030-drops-77310
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7731/
Go to the corresponding LIPIcs Volume Portal

Aoto, Takahito ; Toyama, Yoshihito ; Kimura, Yuta

Improving Rewriting Induction Approach for Proving Ground Confluence

pdf-format:
LIPIcs-FSCD-2017-7.pdf (1 MB)

Abstract

In (Aoto&Toyama, FSCD 2016), a method to prove ground confluence of many-sorted term rewriting systems based on rewriting induction is given. In this paper, we give several methods that add wider flexibility to the rewriting induction approach for proving ground confluence. Firstly, we give a method to deal with the case in which suitable rules are not presented in the input system. Our idea is to construct additional rewrite rules that supplement or replace existing rules in order to obtain a set of rules that is adequate for applying rewriting induction. Secondly, we give a method to deal with non-orientable constructor rules. This is accomplished by extending the inference system of rewriting induction and giving a sufficient criterion for the correctness of the system. Thirdly, we give a method to deal with disproving ground confluence. The presented methods are implemented in our ground confluence prover AGCP and experiments are reported. Our experiments reveal the presented methods are effective to deal with problems for which state-of-the-art ground confluence provers can not handle.

BibTeX - Entry

@InProceedings{aoto_et_al:LIPIcs:2017:7731,
  author =	{Takahito Aoto and Yoshihito Toyama and Yuta Kimura},
  title =	{{Improving Rewriting Induction Approach for Proving Ground Confluence}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{7:1--7:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Dale Miller},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7731},
  URN =		{urn:nbn:de:0030-drops-77310},
  doi =		{10.4230/LIPIcs.FSCD.2017.7},
  annote =	{Keywords: Ground Confluence, Rewriting Induction, Non-Orientable Equations, Term Rewriting Systems}
}

Keywords: Ground Confluence, Rewriting Induction, Non-Orientable Equations, Term Rewriting Systems
Collection: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Issue Date: 2017
Date of publication: 30.08.2017

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