著者
井田 哲雄 MARIN Mircea
出版者
筑波大学
雑誌
挑戦的萌芽研究
巻号頁・発行日
2007

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

折紙における「折る]過程を研究し,以下の成果を得た.(1) 折る過程を抽象的に表現する代数的グラフ書換系を定義し,グラフ書換を記述・実行する言語処理系を開発した.(2) グラフ書換操作から代数系へと変換するアルゴリズムの開発とその正当性の検証を行った.(3) 研究の進展に応じてコンピュータによる折紙実行システムの拡張を行い,折紙幾何定理の証明の高速化と多くの定理の自動証明を可能とした.
著者
井田 哲雄 南出 靖彦 MARIN Mircea 鈴木 大郎
出版者
筑波大学
雑誌
基盤研究(B)
巻号頁・発行日
2008

ウェブソフトウェア検証の事例研究として, WebEosの核となる部分の形式化と検証を行った.幾何と代数の基本的な部分にMathematicaの計算結果を援用することで, 効率的な検証が可能となった.文字列解析による検証において, 正規表現マッチングの正確な解析を可能とした.また, データベースとの連携の解析を導入し, 蓄積型XSS脆弱性検査を実現した.ポジションオートマトンを利用した正規表現の貪欲マッチングアルゴリズムの設計と実装を行った.