2009 Fiscal Year Annual Research Report
| Project/Area Number |
19650001
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
井田 哲雄 University of Tsukuba, 大学院・システム情報工学研究科, 教授 (70100047)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
MARIN Mircea 筑波大学, 大学院・システム情報工学研究科, 講師 (60396603)
|
|---|
| Keywords | 折紙計算論 / 記号計算 / 定理自動証明 / 制約問題 |
|---|
| Research Abstract |
●折紙の理論を構築し,国際雑誌Journal of Symbolic Computationで発表した.この理論では,面の集合と面同士の隣接関係と重なり関係からなる構造により,抽象折紙を定義し,抽象折紙の折り操作を抽象書換え系の書換え操作でモデル化する.さらに,コンピュータの実装に向けて,抽象折紙をラベル付きハイパーグラフで表現し,抽象書換え系をグラフ書き換え系で実現する.さらに,この理論を実装し,本研究の前年度までに構築されているEos(E-Origami System)に組み込んだ.グラフ書き換えのアルゴリズムについても,新たに開発するとともに,アルゴリズムの正当性の基礎になるいくつかの定理を証明した.グラフ書き換えによる折紙の構築過程を可視化することに成功するとともに,折紙をグラフとして見たときの構造の特徴をも明らかにした.
●折紙定理のコンピュータによる自動証明の高速化のために,Eosの定理証明モジュールに様々な方法を組み込んだ.たとえば,証明で用いるグレブナ基底の計算に折紙構築履歴に依存した単項式順序を組み込むこと,折紙幾何に特化した証明ドキュメントの自動生成がある.これらの改良により,折紙定理証明の効率は著しく向上した.たとえば,Morleyの定理の自動証明には当初17時間もかかったが,10分程度で完了するようになった.
●上記EOSシステムのウェブ・インタフェイスの構築研究を継続して行い,ウェブ・インタフェイスの改良をおこなった.
●藤田による折紙の公理をウー・リットの方法で代数的に解釈し直し,折紙の構築の基本操作を与える藤田の公理の代数的な性質を解析した.ウー・リットの手法で用いる特性集合を調べることにより,藤田の公理が記述する幾何の縮退条件を代数的に求めることができた.
|
