| 研究概要 |
平成23年度は次の項目に渉って,研究を推進した.
1.代数的グラフ書換理論による折紙の形式化と正当性を定理証明支援系Isabelleを援用して行う.
2.代数的グラフ書換系を定義し,グラフ書換アルゴリズムを記述・実行するためのグラフ書換言語の設計と実装
3.抽象折り操作をグラフ書換操作で具体化するための,代数系への変換に関する研究
4.研究の進展に応じたEos(E-Origami System,当研究者らが開発し,改良を行っている)システムの拡張
5.多くの実例に当たり,折紙の創作プロセスを折紙プログラムとして記述し,折紙に関する幾何を知識ベース化する研究
項目1については,折紙の基本操作の形式化は完了したが,折紙の構造を抽象化して,当初から想定しているラベル付きのパイパーグラフで表現する部分については,次年度への継続課題となった.正当性証明については,体論から出発すると,証明すべき項目が多く,本研究の範囲を優に超えてしまう.また代数的な操作に関しては,定理証明支援系は本研究を推進するには十分に強力でなく,思いの外研究を進展させるのが困難であることが判明した.項目2,3については,初年度に作業はほぼ完成しており,成果の整理は着実に進んでいる.研究成果の一部は本年度刊行した.項目4については,全研究期間にわたって行われる活動であり,引き続き平成23年度も行った.Eosによって行われる推論過程を系統的にしかも,人が読みやすい形にシステムを拡張し,Proof Documentを生成する機能を実現した.項目5の研究については,次年度で,一層の研究の進展をはかる.
|
