| 研究概要 |
証明アニメーションの諸方式の研究を行った。実際の証明支援系の構築と実験や理論的研究を通して、既存の方法の限界を初めて提示し、それを打ち破る方法として、limiting recursion realizability interpretationと、それによって実現される数学,Limit Computable Mathematics(LCM)の二つを提唱した。具体的内容としては、次のようなものがある。0.証明支援系,ProofWorksの開発と、それによる小方理論の実験。1.抽象計算系ω-BRFにおけるlimiting(partial)functionの定義を、それが再びω-BRFとなることの証明。また、その拡張の可能性の予想。(赤間により実現された)2.limiting(partial)recursive functionによる第1階算術のrealizability.3.これにより、Berardiの例、ヒトベルトの不変式論等が、アニメーション可能であることの確認。また、そのコーディングの方法の研究。(木村,Werner,Herbelinとの共同研究)4.LCMと連続体上のBSS計算理論、八杉のガウス関数の計算可能性の分析との関係。5.LCMによる古典論理の階層理論と逆数字の可能性の発見。(Kolenbach,石原との共同研究)
LCMは注目を集め多くの共同研究を実施できた。これは証明アニメーションが当初の予想を超えた広がりをもつことを示している。Berardi法による証明アニメーション・システムの構築という比較的modestと予想した研究目的は、Berardi法の実行状況の説明を生成することが困難という、予想外の問題に直面し、残念ながら実現することができなかった。しかし、この問題を解決するために得られた研究成果LCMは、当初の計画時には全く予想できなかったものであり、しかも、その広がりは、証明アニメーションを遥かに超えるほどのものであった。これを発展させ、証明アニメーションを証明構築以外の目的にも応用すべく研究を続けている。
|
