• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Study on Ground Confluence of Rewrite Systems

Research Project

Project/Area Number 15K00003
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeMulti-year Fund
Section一般
Research Field Theory of informatics
Research InstitutionNiigata University

Principal Investigator

Aoto Takahito  新潟大学, 自然科学系, 教授 (00293390)

Co-Investigator(Kenkyū-buntansha) 外山 芳人  東北大学, 電気通信研究所, 教授 (00251968)
Project Period (FY) 2015-04-01 – 2018-03-31
Project Status Completed (Fiscal Year 2017)
Budget Amount *help
¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000)
Fiscal Year 2017: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2016: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2015: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Keywords項書き換えシステム / 基底合流性 / 書き換え帰納法 / 基底合流生
Outline of Final Research Achievements

Ground confluence of term rewriting systems is a property fundamental to establish software verification techniques based on rewrite systems. In this study, we have focused on rewriting induction which a method for inductive theorem proving, and have shown that bounded convertibility guarantees the ground confluence. We have designed a rewriting induction method for establishing bounded convertibility and have shown its correctness theoretically. We have also given a method to deal with the case in which suitable rules are not presented in the input system, a method to deal with non-orientable constructor rules, and a method to deal with disproving ground confluence. Based on the proposed methods we have implemented in ground confluence prover AGCP.

Report

(4 results)
  • 2017 Annual Research Report   Final Research Report ( PDF )
  • 2016 Research-status Report
  • 2015 Research-status Report
  • Research Products

    (12 results)

All 2018 2017 2016 2015 Other

All Journal Article (8 results) (of which Peer Reviewed: 8 results,  Open Access: 4 results,  Acknowledgement Compliant: 6 results) Presentation (3 results) Remarks (1 results)

  • [Journal Article] Improving rewriting induction approach for proving ground confluence2017

    • Author(s)
      Takahito Aoto, Yoshihito Toyama and Yuta Kimura
    • Journal Title

      Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction

      Volume: 84

    • DOI

      10.4230/LIPIcs.FSCD.2017.7

    • Related Report
      2017 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Parallel Closure Theorem for Left-Linear Nominal Rewriting Systems2017

    • Author(s)
      Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama
    • Journal Title

      Proceedings of the 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017)

      Volume: 10483 Pages: 115-131

    • DOI

      10.1007/978-3-319-66167-4_7

    • ISBN
      9783319661667, 9783319661674
    • Related Report
      2017 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Ground confluence prover based on rewriting induction2016

    • Author(s)
      Takahito Aoto and Yoshihito Toyama
    • Journal Title

      In Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction, Porto, Portugal

      Volume: 52

    • DOI

      10.4230/LIPIcs.FSCD.2016.33

    • Related Report
      2016 Research-status Report
    • Peer Reviewed / Open Access / Acknowledgement Compliant
  • [Journal Article] Nominal confluence tool2016

    • Author(s)
      Takahito Aoto and Kentaro Kikuchi
    • Journal Title

      Proceedings of the 8th International Joint Conference on Automated Reasoning, Coimbra, Portugal

      Volume: 9706 Pages: 173-182

    • Related Report
      2016 Research-status Report
    • Peer Reviewed / Acknowledgement Compliant
  • [Journal Article] Decision Method of Reachability based on Rewrite Rule Overlapping2016

    • Author(s)
      島貫健太郎, 青戸等人, 外山 芳人
    • Journal Title

      Computer Software

      Volume: 33 Issue: 3 Pages: 3_93-3_107

    • DOI

      10.11309/jssst.33.3_93

    • NAID

      130005256734

    • ISSN
      0289-6540
    • Related Report
      2016 Research-status Report
    • Peer Reviewed / Acknowledgement Compliant
  • [Journal Article] Critical Pair Analysis in Nominal Rewriting2016

    • Author(s)
      Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama
    • Journal Title

      Proceedings of 7th SCSS

      Volume: 39 Pages: 156-168

    • Related Report
      2015 Research-status Report
    • Peer Reviewed / Open Access / Acknowledgement Compliant
  • [Journal Article] Confluence of orthogonal nominal rewriting systems revisited2015

    • Author(s)
      Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama
    • Journal Title

      Proceedings of 26th RTA

      Volume: 36 Pages: 301-317

    • DOI

      10.4230/LIPIcs.RTA.2015.301

    • Related Report
      2015 Research-status Report
    • Peer Reviewed / Open Access / Acknowledgement Compliant
  • [Journal Article] Correctness of context-moving transformations for term rewriting systems2015

    • Author(s)
      Koichi Sato, Kentaro Kikuchi, Takahito Aoto and Yoshihito Toyama
    • Journal Title

      Proceedings of 25th LOPSTR

      Volume: 9527 Pages: 331-345

    • DOI

      10.1007/978-3-319-27436-2_20

    • ISBN
      9783319274355, 9783319274362
    • Related Report
      2015 Research-status Report
    • Peer Reviewed / Acknowledgement Compliant
  • [Presentation] 条件付き項書き換えシステムにおけるホーン節帰納的定理の自動証明2018

    • Author(s)
      栗田泰智,青戸等人
    • Organizer
      第20回プログラミングおよびプログラミング言語ワークショップ
    • Related Report
      2017 Annual Research Report
  • [Presentation] 書き換え帰納法を利用した帰納的定理証明の補題生成法2017

    • Author(s)
      加藤裕人,青戸等人
    • Organizer
      日本ソフトウェア科学会第34回大会
    • Related Report
      2017 Annual Research Report
  • [Presentation] 極大完備化に基づく等式定理の自動証明2017

    • Author(s)
      萩原崇央,青戸等人
    • Organizer
      日本ソフトウェア科学会第34回大会
    • Related Report
      2017 Annual Research Report
  • [Remarks] 青戸研究室ウェブページ

    • URL

      http://www.nue.ie.niigata-u.ac.jp/

    • Related Report
      2017 Annual Research Report 2016 Research-status Report

URL: 

Published: 2015-04-16   Modified: 2019-03-29  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi