Study on Ground Confluence of Rewrite Systems

2017 Fiscal Year Final Research Report

• Project/Area Number: 15K00003
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Theory of informatics
• Research Institution: Niigata University
• Principal Investigator: Aoto Takahito 新潟大学, 自然科学系, 教授 (00293390)
• Co-Investigator(Kenkyū-buntansha): 外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
• Project Period (FY): 2015-04-01 – 2018-03-31
• 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.

Free Research Field

プログラム理論