| 研究概要 |
本年度はBerardi法の研究が進んだ。その成果は以下の(i),(ii),(iii)である。
(i)Berardi法、すなわち、Berardiの古典論理の近似理論の分析は、Berardi理論の難解さのために難航を極めたが、ようやく証明アニメーションへの応用に目処がつき、理論研究の突破口となった。また、その方法による証明アニメーションのモックアップ・アプレットなども作成した。
(ii)この分析の結果、Berardi法の適用範囲は学習理論の基礎論とされるGoldのlimiting recursionと一致するらしいことを発見した。学習理論との関係は予想外の成果である。これにより、Berardi法、八杉等の不連続関数の計算可能性解析学、limited principle of omniscience(σ^0_1命題に対しての排中律)をもととする証明アニメーションを統合する理論の可能性が開け、多くの数学的理論が、この理論の応用範囲に属すであろうことが予測できるようになった。今後は、この新しい知見を中心にしてBerardi法による証明アニメーションの理論体系を構築する予定である。Gold理論との関係は、証明アニメーションの研究を超えて、数学、計算機科学等におけるconstructivityの概念の拡張にもつながる可能性があり非常に重要なものと考えるので、この方向の研究も行う予定である。
(iii)代数学において本質的に超限的方法(古典論理による証明方法)が使用された最初の例の一つとされるヒルベルトの不変式論が、この方法によりアニメーションできる可能性が非常に高いことを発見した。そこで最初の本格的ケーススタディーとして、この理論の形式化を行うことにし、仏国INRIA,Coq groupのB.Werner,H.Herbelin氏に協力を要請し、Coq上でのヒルベルトの不変式論実現の計画を開始した。
|
