2011 Fiscal Year Annual Research Report
代数的グラフ書換理論に基づく折紙のモデル化と折紙プログラミング
| Project/Area Number |
22650001
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
井田 哲雄 筑波大学, システム情報系, 教授 (70100047)
|
|---|
| Keywords | 計算折紙論 / 記号計算 / 自動幾何定理証明 / グラフ書換系 |
|---|
| Research Abstract |
平成23年度は次の項目に渉って,研究を推進した.
1.代数的グラフ書換理論による折紙の形式化と正当性を定理証明支援系Isabelleを援用して行う.
2.代数的グラフ書換系を定義し,グラフ書換アルゴリズムを記述・実行するためのグラフ書換言語の設計と実装
3.抽象折り操作をグラフ書換操作で具体化するための,代数系への変換に関する研究
4.研究の進展に応じたEos(E-Origami System,当研究者らが開発し,改良を行っている)システムの拡張
5.多くの実例に当たり,折紙の創作プロセスを折紙プログラムとして記述し,折紙に関する幾何を知識ベース化する研究
項目1については,折紙の基本操作の形式化は完了したが,折紙の構造を抽象化して,当初から想定しているラベル付きのパイパーグラフで表現する部分については,次年度への継続課題となった.正当性証明については,体論から出発すると,証明すべき項目が多く,本研究の範囲を優に超えてしまう.また代数的な操作に関しては,定理証明支援系は本研究を推進するには十分に強力でなく,思いの外研究を進展させるのが困難であることが判明した.項目2,3については,初年度に作業はほぼ完成しており,成果の整理は着実に進んでいる.研究成果の一部は本年度刊行した.項目4については,全研究期間にわたって行われる活動であり,引き続き平成23年度も行った.Eosによって行われる推論過程を系統的にしかも,人が読みやすい形にシステムを拡張し,Proof Documentを生成する機能を実現した.項目5の研究については,次年度で,一層の研究の進展をはかる.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
対象への理解が深まっており,それに伴い,ソフトウェア及び論文として研究成果の蓄積が進んでいる.
|
| Strategy for Future Research Activity |
研究を推進する上で,ソフトウェアの開発や蓄積が不可欠であるため,これに割くべき人的リソースを充実させ,十分に確保することが重要になってくる.
研究を推進する上で不可欠な定理証明支援系と記号代数系ソフトウェアとの連携がより重要になってくるとの認識を得た.
|
