| Project/Area Number |
22700009
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
HIROKAWA Nao 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (50467122)
|
|---|
| Research Collaborator |
MIDDELDORP Aart University of Innsbruck, Institute for Computer Science, Professor
KLEIN Dominik 北陸先端科学技術大学院大学, 情報科学研究科, 博士後期課程学生(当時)
|
|---|
| Project Period (FY) |
2010 – 2012
|
| Project Status |
Completed (Fiscal Year 2012)
|
| Budget Amount *help |
¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
Fiscal Year 2012: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2011: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2010: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
|
|---|
| Keywords | 項書換え / 合流性 / 完備化 / 戦略 / 計算理論 / 関数型プログラム |
|---|
| Research Abstract |
Term rewriting is a computational model which underlies functional programming and theorem proving. In this research project we revisited its fundamental theory in the light of relative termination. As an outcome, we established a new confluence criterion that unifies two major confluence criteria (Rosen’s orthogonality and Knuth and Bendix’ completeness) for left-linear systems. Moreover, we introduced a new technique for automated deduction, dubbed maximal completion. Based on those new technologies, we developed the powerful confluence analyzer Saigawa and the fully automatic completion tool Maxcomp.
|
