| 研究概要 |
計算折紙理論の厳密化を進めた.まず,理論の基礎となる藤田の折紙原理を見直し,折紙原理を構成する,各折り操作を縮退条件も含めて論理的に厳密に構成した,これを基に定理証明支援系での形式化を進めた.定理証明支援系は形式化に用いる論理体系により,記述の簡明さや表現力に違いがでてくるため,基礎概念をいくつかの体系で記述することを試みた.具体的には,Coq, Isabelle/HO, HOL/Lightを用いで,形式化を試みた.さらにカリシックが昨年来、進めてきた,商集合を用いた形式化手法を,線の概念の形式化に用いて,藤田の折紙原理および,それに基づいて成立する主な幾何定理の形式化と証明の簡素化と抽象化を進めた.また,幾何学の定理証明には代数的なアプローチとの併用が欠かせないため,代数記号計算システムとの連携についても考察を深めた.代数計算の部分については,これまでブラックポックスとして用いてきたが,この部分についても,定理証明系からアルゴリズムの検証が可能になるよう,代数計算の見直しを行った.また,代数記号計算システムと定理証明支援系を十分な速度で稼働させるために,ソフトウェア環境の整備や証明ドキュメントの生成などのソフトウェア構築も行った.構築したソフトウェアの一部は井田らが開発してきた計算折紙システムEOSに組み込んだ研究成果は,ACM Symposium on Applied Computing SAC2011で発表した.異なるトラックで二件の発表を行った.一件は商集合の展開に関して,もう一件は藤田の折紙原理の拡張についてである.
|
