| 研究概要 |
折紙と折紙の作成過程のモデル化をグラフ書換系を用いて行った.折紙は,二つの表面から成る面と,面同士の重なり関係と隣接関係でモデル化できる.このモデルを一般化するとグラフ構造が得られる.このグラフ構造は,面の集合とその上の二つの二項関係の組の実現であるので,ラベル付きハイパーグラフとして実現した.折紙の作成は,このラベル付きハイパーグラフの書換として形式化した.このモデルを我々の開発したEos(E-Origami System)とよぶシステムに追加する形で実装し,形式化の正当性や効率,計算の複雑度などを検討した.形式化に関しては,定理証明支援系を用いて,厳密に行うことを目指しており,定理証明支援系の比較検討や,関連する研究の調査を行い,次年度に本格的に行う,定理証明支援系による形式化の準備を整えた.これと並行して,折り方の基本原理について,根本から考え直す作業を行った.基本原理には藤田の原理と呼ばれるものが知られているが,これを厳密化し,縮退条件を明確化し,原理を構成する一つ一つの操作の関連性について,より正確な議論を展開した.新しい折紙の原理についてもEosシステムに実装し,システムの公開を行った.
本研究における折紙操作のモデル化よって得られる成果の応用には,折紙に関する幾何定理の自動証明や,折り方の新たな知見の工業技術への組み込みが考えられるが,前者については,今年度の研究で大きな成果が得られている.すなわち,Eosシステムの定理自動証明システムの機能の拡張を行い,定理自動証明の過程を克明に,しかも構造化された形で表現する証明ノートの自動生成や自動証明の高速化に必要な様々な機能拡張をおこなった.上で述べた,公開Eosシステムにはこの機能がすでに盛り込まれている.
|
