証明アニメーション(構成的プログラミングによる証明テスト技法)

1999 Fiscal Year Annual Research Report

• Project/Area Number: 10480063
• Research Institution: Kobe University
• Principal Investigator: 林 晋 神戸大学, 工学部, 教授 (40156443)
• Co-Investigator(Kenkyū-buntansha): 佐藤 雅彦 京都大学, 大学院・工学研究科, 教授 (20027387) ; 八杉 満利子 京都産業大学, 理学部, 教授 (90022277) ; 田村 直之 神戸大学, 工学部, 助教授 (60207248)
• Keywords: 形式的証明の開発 / 定理証明 / 論理情報の視覚化 / 古典論理証明の実行 / Curry-Howardの対応

Research Abstract

本年度は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上でのヒルベルトの不変式論実現の計画を開始した。

Research Products

• [Publications] S.Hayashi: "Towerds Animation of Proofs"Theoretical Computer Science. (未定). (2000)
• [Publications] M.Yasugi: "Effective properties of sets and functions in metric spaces with computability structure"Theoretical Computer Science. 219. 467-486 (1999)