2012 Fiscal Year Final Research Report
Research on automated confluence proving for term rewriting systems
| Project/Area Number |
22500002
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
AOTO Takahito 東北大学, 電気通信研究所, 准教授 (00293390)
|
|---|
| Project Period (FY) |
2010 – 2012
|
| Keywords | 書き換えシステム / 合流性 / 自動検証 / 停止性 / モジュラ性 |
|---|
| Research Abstract |
The theory of term rewriting systems is widely used in the fields of automated theorem provings and computation models. Although many automated termination provers of term rewriting systems have been proposed recently, little work is reported on automated confluence provers. This research aims to develop an automated confluence prover ACP for term rewriting systems based on several methods. Concrete results include a reduction-preserving completion method for proving confluence, one side decreasing diagram method for proving commutativity, a path ordering for guaranteeing polynomial size normal forms, a confluence proof method based on persistency. In the first confluence competition for term rewriting systems (IWC 2012), ACP developed by our group has won first place among the three participants.
|
