2013 Fiscal Year Research-status Report
立体折紙の計算理論の展開と計算折紙ソフトウェアの開発
| Project/Area Number |
25330007
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
井田 哲雄 筑波大学, 名誉教授 (70100047)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | 自動定理証明 / プログラム検証 / 計算折紙 / 記号計算 / 立体折紙 / 計算幾何 |
|---|
| Research Abstract |
グラフ書換理論に基づく立体折紙の計算モデルの研究を推進した．より抽象的にモデルをとらえて数理科学の全般への貢献を目指す方向性と，コンピュータによる効率の良い実装を目指す方向性をもたせて，研究を進めた 立体折紙のモデルは，法線ベクトルが同一の平面の集まり（これを，層（sheaf）と呼ぶ）から構成される．各平面には，凸多角形の形状を持つ折紙面が配置され，折紙面同士には，上下関係と隣接関係が定義される．このモデルは，一つの「折り」によって，逐一変換を受け，新たなモデルが生成される．変換は，層を構成する折紙面の上下関係，隣接関係の変更のみならず，折紙面の変形をもたらすために，一般には複雑な操作となる．このため，モデルをグラフによって表現し，グラフの書換によって，操作を実現している．
本研究は，実施研究者が高橋英和（滋賀県立八日市高校）とファドア・ゴーラビ（関西学院大学）と共同で開発を進めているEOS(e-Origami System)と呼ぶ計算折紙システムの高次化としても位置づけ，新しい折紙の課題を取り上げつつ，モデルの適切性の検証と，計算折紙に関する新たな科学的知見の獲得を目指して，研究を進めている．
上に述べたモデル化の試みに加え，次の二つの研究成果を得た．定理証明支援系Isabelle/HOLを用いて，EOSプログラムの一部の形式化と検証を行った．結び目折りの解析を行った．結び目折りを一階述語論理の言語で表現し，制約解消により結び目の自動生成と検証に成功した．結び目折りは，従来の平面折紙だけでは表現しきれず，面の重なりを立体折紙の視点から検討する必要がある．結び目折りに関しては，二つの国際会議で発表した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究課題を以下の４項目に分けて進めており，各項目について，順調に研究が進展している．(1)立体折紙をモデル化するグラフ書換理論の構築，(2)抽象的にとらえた折り操作をグラフ書換操作で具体化するための手法に関する研究，(3)グラフ書換系の基本操作のコンピュータへの実装，(4)研究の進展に応じたEOSシステムの立体折紙への拡張，これらは順を追って遂行するのではなく，単純な問題から，より一般化された問題へと，（１）～（４）のステップを繰り返しつつ，研究を進展させている．
|
| Strategy for Future Research Activity |
研究計画の当初通りである．グラフ書換え系については，立体折紙への応用が重要であるので，グラフ書換え系を独立して研究するよりも，計算折紙への応用に即した形式化を進めていく．
研究成果の発表の時期，場所（国際会議）については，この分野の国際的動向に応じて適切な方法を考えたい．
|
Research Products
(4 results)
