記号計算の手法を用いた折り紙計算論の構築

点击翻译按钮获取中文摘要

本研究では,記号計算の手法を駆使して,折紙の数理を制約解消および定理自動証明の側面から探求した.具体的には,記号計算の手法を駆使して,折紙の計算理論の構築と理論に基づいた折紙計算環境の実現をはかった.2年間の研究実施期間中に,これまでに知られる折紙による幾何オブジェクトの構成例の多くを,制約解消問題として再構成し,さらに,構成の正しさを定理自動証明システムを用いて証明した.本研究のすべてのフェースにわたって,計算機による支援は不可欠であるため,並行して,計算論的折紙計算環境構築をすすめた.上記研究目標への到達を目指して,17年度から推進している次の3つの課題について,18年度も継続して研究を推進した.1.Huzitaの折紙公理として知られる折紙構成法を出発点とする折紙計算論の構築.これに関しては,Huzitaの折紙公理を記述する多ソート一階述語論理の体系を定め,インフォーマルに与えられてきた6つの公理を形式的に記述した.さらに,各公理の代数的な解釈を与えた.この解釈により,折紙の数理研究の基礎が得られ,折紙の定理証明の自動化が可能となった.2.幾何定理自動証明系を活用した,折紙に関する諸性質の形式化と自動証明.これに関しては,具体的な折紙作図の問題に取り組み,BuchbergerアルゴリズムとCylindrical Algebraic Decompositionのアルゴリズムを適用し,最大正三角形の折紙作図問題の自動定理証明に成功した.3.折紙の操作アルゴリズムの開発と折り紙計算論を支援する折り紙計算環境の構築.折紙の操作と折紙の定理証明を系統的に結合するために,記号計算の観点から,データ構造やアルゴリズムを再検討した.これにより,幾何定理自動証明系と制約解消系との整合性のとれた,折紙研究環境を実現できた.このシステムをEos(E-origami System)と名付けた.今後の実用化に向けてさらに改良を図る予定である.