| 研究課題/領域番号 |
10480063
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 神戸大学 |
|---|
研究代表者 |
林 晋 神戸大学, 工学部, 教授 (40156443)
|
|---|
| 研究分担者 |
佐藤 雅彦 京都大学, 大学院・工学研究科, 教授 (20027387)
八杉 満利子 京都産業大学, 理学部, 教授 (90022277)
田村 直之 神戸大学, 工学部, 助教授 (60207248)
|
|---|
| 研究期間 (年度) |
1998 – 2000
|
| 研究課題ステータス |
完了 (2000年度)
|
| 配分額 *注記 |
6,300千円 (直接経費: 6,300千円)
2000年度: 1,300千円 (直接経費: 1,300千円)
1999年度: 1,500千円 (直接経費: 1,500千円)
1998年度: 3,500千円 (直接経費: 3,500千円)
|
|---|
| キーワード | 形式的証明の開発 / 定理証明 / 論理情報の視覚化 / 古典論理証明の実行 / Curry-Howardの対応 / 学習理論 |
|---|
| 研究概要 |
証明アニメーションの諸方式の研究を行った。実際の証明支援系の構築と実験や理論的研究を通して、既存の方法の限界を初めて提示し、それを打ち破る方法として、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は、当初の計画時には全く予想できなかったものであり、しかも、その広がりは、証明アニメーションを遥かに超えるほどのものであった。これを発展させ、証明アニメーションを証明構築以外の目的にも応用すべく研究を続けている。
|
