記号計算の手法を駆使した証明とアルゴリズムの形式化

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

定理証明支援系(以下PAと略す)とコンピュータ代数系(以下CAと略す)の融合の必要性については,多くの先進的研究者の指摘するところであるが,これまで対象としてきた分野が純粋数学に限られており,その有効性や可能性が他の分野,特に最も適用が期待されるソフトウェア工学の分野にまで波及していない.本研究では,対象を幾何やコンピュータグラフィックスにまで広げ,PAとCAの融合の有効性を示すとともに,対象分野,特に幾何の概念および幾何オブジェクトの操作アルゴリズムの厳密化をはかった.計算折紙理論は,最近本研究の推進者らによって,厳密化されてきているが,この研究をさらに進展させることを目指した.まず,理論の基礎となる藤田の折紙原理を,PAによって形式化した.形式化に用いる論理体系により,記述の簡明さや表現力に違いがでてくるため,基礎概念を代表的PAであるCoqとIsabelle/HOLで記述することを試みた.さらにカリチェクが昨年来、進めてきた,商集合を用いた形式化手法を,線の概念の形式化に用いることとし,藤田の折紙原理および,それに基づいて成立する主な幾何定理の形式化と証明の簡素化と抽象化を進めた.また,CAにはMathematicaを用いた.予想通り,CAのみに頼る検証は困難であり,様々なところで代数的な考察が必要になった.代数表現に関する推論は,PAでは十分に行えず,CAによる式の変形をPAに公理として導入する必要があった.このようなPAとCAの結合(ないしは融合は)は,現在のところ自動化することは難しく,さらなく研究が必要とされる.