| 研究課題/領域番号 |
25730004
|
|---|
| 研究種目 |
若手研究(B)
|
| 配分区分 | 基金 |
|---|
| 研究分野 |
情報学基礎理論
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
廣川 直 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (50467122)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| 研究課題ステータス |
完了 (2015年度)
|
| 配分額 *注記 |
3,900千円 (直接経費: 3,000千円、間接経費: 900千円)
2015年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2014年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2013年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
|
|---|
| キーワード | 項書換え / 合流性 / 国際研究者交流 / オーストリア / 可換性 / 形式言語 |
|---|
| 研究成果の概要 |
項書換えシステムは定理自動証明や仕様記述言語の基盤理論であり、演繹や計算は等式変形による答えの網羅的な探索として実現される。そのため計算結果が必ず一意に定まることを保証する合流性は、効率な計算の実現に大切な性質である。本研究では合流性の証明手法とその応用に取り組み以下の成果を得た：（１）可換性分解、危険対解析、Ｅ単一化に関する技法を開発・発展させ、強力な合流性解析を実現した。（２）それらの知見の応用として、定理自動証明の基盤理論である抽象完備化の正当性についての簡潔な証明、（３）さらに計算を効率的に行うための基本正規化定理を得た。
|
