2012 Fiscal Year Final Research Report
Rewriting Techniques for Non-Deterministic Computation
| 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
|
| 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.
|
Research Products
(11 results)
