| 研究概要 |
本年度は,Proof Animation(以下PA)の基本コンセプトの洗練化とモデル化を行い、支援システムProofWorks,ProofWorks-Classicsの実装とそれ上の実験を行った。
構成的数学用の支援システムproofWorksは、証明記述・構築モジュール、プログラム抽出モジュールが完成した。また、これを元にETL小方の理論による古典数学用システムProofWorks-Classicsを実装した。ProofWorks-Classicsは、証明記述・構築、プログラム抽出が古典論理化され、さらにProofWorksに欠けているプログラムの実行系も実装された。ProofWorksでは、証明とプログラムが有機的に結合されているが、Classicsでは、これは未完成である。ProofWorks-classicsでは、線形論理に基づく古典論理系がつかわれている。
PAの基本コンセプトの洗練化としては、PAを定義、定理、推論の各アニメーションに分類し、その条件を検証した。数学的帰納法を使うと、有限個の碁石は常に同色であることを証明できる(ように見える)という、数理パズルを使ってケーススタディを行った。この特定の問題に対してJAVA appletによりPAの視覚化を行い、さらに、同問題をProofWorks,ProofWorks-Classicsにより形式化し、プログラムの抽出と実行による証明のトレースの実験を行った。この実験や先に述べたアプレットを検討した結果、問題の視覚化により抽出されたプログラムを見ることなく、証明のバグを発見できることが判明した。これは予想しなかった成果であり、来年度以降主要な研究テーマとする予定。また、八杉らが計算可能解析学の研究中で提出したガウス関数の例が、PAに面白い例を提供し、さらに、この場合のようなサーチ原理を元に構成的PAを古典化するという方法をCoq project Paulin教授より示唆された。これらを統合して、non-trivialなPAのケーススタディを目指したい。
|
