2011 Fiscal Year Final Research Report
Proving confluence of higher-order term rewriting systems automatically
| Project/Area Number |
21700017
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Shimane University |
|---|
Principal Investigator |
|
|---|
| Project Period (FY) |
2009 – 2011
|
| Keywords | 項書換えシステム / 高階項書換えシステム / 無限項書換えシステム / 合流性 / 強頭部正規化可能性 / 強収束性 / 生成性 / 一般生成性 |
|---|
| Research Abstract |
We studied several rewriting systems for proving confluence of higher-order term rewriting systems automatically. In this project, we showed many term rewriting systems of combinators do not have strong head normalization. Furthermore, we presented procedures for disproving two properties of infinitary term rewriting systems. the strong head normalization and the productivity. The correctness of our procedures is proved. And we implemented our procedures.
|
