2005 Fiscal Year Annual Research Report
| Project/Area Number |
17650003
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
井田 哲雄 筑波大学, 大学院・システム情報工学研究科, 教授 (70100047)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
MARIN Mircea 筑波大学, 大学院・システム情報工学研究科, 講師 (60396603)
|
|---|
| Keywords | 計算折紙 / 定理自動証明 / グロブナ基底 / ソフトウェア検証 |
|---|
| Research Abstract |
次の3つの課題について,研究を推進した.
1,Huzitaの折り紙公理として知られる折り紙構成法を出発点とする折り紙計算論の構築
2,幾何定理自動証明系を活用した,折り紙に関する諸性質の形式化と自動証明
3,折り紙の操作アルゴリズムの開発と折り紙計算論を支援する折り紙計算環境の構築
課題1に関して
Huzitaの折り紙公理は6つの構成法よりなっている.この構成法は定規とコンパスを用いたユークリッド幾何オブジェクトの構成法より強力であることが知られている.定規とコンパスによる構成法を越える能力を折り紙が持つのは,折り紙では,すでにある折れ目に沿って,点をずらしながら,折り線を決めることができることにある.Huzitaの折り紙公理の第6公理が,これを表現している.この構成法をさらに,拡張し「高階」折り紙構成法の理論を構築した.
課題2に関して
高次の多項式系の求解にはグロブナ基底を計算するBuchbergerアルゴリズムが用いられる.さらに,折り紙の定理の証明にも,Buchbergerアルゴリズムが用いられる.折り紙の操作と折り紙の定理証明を系統的に結合するためには,記号計算の観点から,データ構造やアルゴリズムの整理が必要になってくる.幾何定理自動証明系を活用しつつ,証明系と制約解消系との整合性のとれた,折り紙の内部表現のデザインをすすめた.
課題3に関して
折り紙計算論を支援するには,折り紙の操作を実際に計算機で実現できることが重要である.このため,Eos(E-origami System)と呼ぶ計算折紙システムの構築を進めた.
|
