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
|
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)
Research Products
(12 results)