2017 Fiscal Year Final Research Report
Study on Ground Confluence of Rewrite Systems
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 |
プログラム理論
|