Improving rewriting induction approach for proving ground confluence

Takahito Aoto, Yoshihito Toyama, Yuta Kimura

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)

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.

Original languageEnglish
Title of host publication2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017
EditorsDale Miller
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959770477
DOIs
Publication statusPublished - 2017 Sep 1
Event2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017 - Oxford, United Kingdom
Duration: 2017 Sep 32017 Sep 9

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume84
ISSN (Print)1868-8969

Other

Other2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017
CountryUnited Kingdom
CityOxford
Period17/9/317/9/9

Keywords

  • Ground confluence
  • Non-orientable equations
  • Rewriting induction
  • Term rewriting systems

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Improving rewriting induction approach for proving ground confluence'. Together they form a unique fingerprint.

  • Cite this

    Aoto, T., Toyama, Y., & Kimura, Y. (2017). Improving rewriting induction approach for proving ground confluence. In D. Miller (Ed.), 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017 [7] (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 84). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.FSCD.2017.7