| 研究課題/領域番号 |
10480063
|
|---|
| 研究機関 | 神戸大学 |
|---|
研究代表者 |
林 晋 神戸大学, 工学部, 教授 (40156443)
|
|---|
| 研究分担者 |
佐藤 雅彦 京都大学, 大学院・工学研究科, 教授 (20027387)
八杉 満利子 京都産業大学, 理学部, 教授 (90022277)
田村 直之 神戸大学, 工学部, 助教授 (60207248)
|
|---|
| キーワード | 形式的証明の開発 / 定理証明 / 論理情報の視覚化 / 古典論理証明の実行 / Curry-Howardの対応 / 学習理論 |
|---|
| 研究概要 |
古典論理実行の新しい方式として、limiting recursion realizability interpretationと、それによって実現される数学,Limit Computable Mathematics(LCM)の、二つの開発を行った。具体的内容としては、次のようなものがある。1.抽象計算系ω-BRFにおけるlimiting(partial)functionの定義と、それが再びω-BRFとなることの証明。また、その拡張の可能性の予想(赤間により実現された。)。2.limiting(partial)recursive functionによる第1階算術のrealizability.3.これにより、Berardiの例、ヒルベルトの不変式論等が、アニメーション可能であることの確認。(木村との共同研究)4.LCMと連続体上のBSS計算理論、八杉のガウス関数の計算可能性の分析との関係。5.LCMによる古典論理の階層理論と逆数学の可能性の発見。(Kolenbach,石原との共同研究)
LCMは注目を集め多くの共同研究を実施できた。その中から、赤間のPCFのlimitingの研究、林が予想した古典論理の階層の存在の、Kohlenbachによる証明、林のlimiting recursive realizabilityに発想を得たBerardiの新解釈などが生まれた。これらは証明アニメーションが当初の予想を越えた広がりをもつことを示している。
Berardi法による証明アニメーション・システムの構築という比較的modestと予想した研究目的は、Berardi法の実行状況の説明を生成することが困難という、予想外の問題に直面し、残念ながら実現することができなかった(証明チェッカー構築の遅れもある)。しかし、この問題を解決するために得られた研究成果LCMは、当初の計画時には全く予想できなかったものであり、しかも、その広がりは、証明アニメーションを遥かに超えるほどのものであった。これを発展させ、証明アニメーションを証明構築以外の目的にも応用すべく研究を続けている。
|
