Confluence Analysis for Term Rewriting and Its Applications

2015 Fiscal Year Final Research Report

• Project/Area Number: 25730004
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Multi-year Fund
• Research Field: Theory of informatics
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: Hirokawa Nao 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (50467122)
• Project Period (FY): 2013-04-01 – 2016-03-31
• Keywords: 項書換え / 合流性 / 国際研究者交流 / オーストリア

Outline of Final Research Achievements

Term rewriting is a fundamental computational model that underlies automated theorem proving and algebraic specification languages. In applications, deduction or computation is usually performed as an exhaustive search of normal forms. Therefore, for efficient computation, confluence that guarantees uniqueness of normal forms is considered as one of the most important properties in the area of rewriting. The main outcomes of our project are three: (1) We developed effective confluence analysis based on commutative decomposition, critical pair analysis, and E-unification. As applications of confluence analysis, (2) we obtained a simple proof for correctness of abstract completion which is a theoretical foundation of automated theorem proving, and also (3) a basic normalization theorem that enables us to effectively compute a normal form of basic terms.

Free Research Field

項書換え